Publications

For all self-archived versions linked below, please consider the link to the publisher’s final authenticated version contained in the PDF documents.

(2020). REFINITY to Model and Prove Program Transformation Rules. Proc. APLAS 2020.

(2020). Treating for-Loops as First-Class Citizens in Proofs. Computing Research Repository (CoRR).

PDF

(2020). Abstract Execution: Automatically Proving Infinitely Many Programs. TUPrints, Technical University of Darmstadt, Department of Computer Science.

PDF DOI

(2019). Verifying OpenJDK's Sort Method for Generic Collections. J. Autom. Reasoning.

DOI

(2019). The Trace Modality. Proc. Second Intern. Workshop on Dynamic Logic. New Trends and Applications (DaLí).

PDF DOI

(2019). Technical Report: Using Loop Scopes with for-Loops. Computing Research Repository (CoRR).

PDF

(2019). Abstract Execution. Proc. Third World Congress on Formal Methods - The Next 30 Years, (FM).

PDF DOI

(2018). Modular, Correct Compilation with Automatic Soundness Proofs. Proc. 8th Intern. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA).

PDF DOI

(2017). A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows. Proc. 13th Intern. Conf. on Integrated Formal Methods (IFM).

PDF DOI

(2016). A General Lattice Model for Merging Symbolic Execution Branches. Proc. 18th Intern. Conf. on Formal Engineering Methods (ICFEM).

PDF DOI