| Publication | Date of Publication | Type |
|---|
| Quicksort revisited. Verifying alternative versions of quicksort | 2021-05-20 | Paper |
An assertional proof of the stability and correctness of Natural Mergesort
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Behavioral interface specification languages
ACM Computing Surveys | 2014-08-13 | Paper |
Automating theorem proving with SMT
Interactive Theorem Proving | 2013-08-07 | Paper |
Stepwise refinement of heap-manipulating code in Chalice
Formal Aspects of Computing | 2013-03-22 | Paper |
Automating Induction with an SMT Solver
Lecture Notes in Computer Science | 2012-06-15 | Paper |
Doomed program points
Formal Methods in System Design | 2011-03-31 | Paper |
Dafny: an automatic program verifier for functional correctness
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Deadlock-free channels and locks
Programming Languages and Systems | 2010-05-04 | Paper |
A polymorphic intermediate verification language: design and logical encoding
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
A logic of object-oriented programs
Lecture Notes in Computer Science | 2010-03-23 | Paper |
Efficient weakest preconditions
Information Processing Letters | 2009-08-27 | Paper |
A Basis for Verifying Multi-threaded Programs
Programming Languages and Systems | 2009-03-31 | Paper |
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
Lecture Notes in Computer Science | 2008-12-04 | Paper |
Verification of Equivalent-Results Methods
Programming Languages and Systems | 2008-04-11 | Paper |
| A verifying compiler for a multi-threaded object-oriented language | 2008-03-06 | Paper |
Using History Invariants to Verify Observers
Programming Languages and Systems | 2007-09-04 | Paper |
Specification and verification challenges for sequential object-oriented programs
Formal Aspects of Computing | 2007-08-23 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2006-10-20 | Paper |
FM 2005: Formal Methods
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2005-12-06 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Generating error traces from verification-condition counterexamples
Science of Computer Programming | 2005-05-12 | Paper |
| scientific article; zbMATH DE number 1982200 (Why is no real title available?) | 2003-09-16 | Paper |
| scientific article; zbMATH DE number 1832224 (Why is no real title available?) | 2002-11-19 | Paper |
Virginity: A contribution to the specification of object-oriented software
Information Processing Letters | 2002-08-04 | Paper |
Annotation inference for modular checkers
Information Processing Letters | 2002-07-25 | Paper |
| scientific article; zbMATH DE number 1693447 (Why is no real title available?) | 2002-01-22 | Paper |
A semantic approach to secure information flow
Science of Computer Programming | 2000-06-04 | Paper |
Computing permutation encodings
Formal Aspects of Computing | 2000-01-02 | Paper |
| scientific article; zbMATH DE number 1251179 (Why is no real title available?) | 1999-06-07 | Paper |
Joining specification statements
Theoretical Computer Science | 1999-04-28 | Paper |
Constructing a program with exceptions
Information Processing Letters | 1997-02-28 | Paper |
Conditional composition
Formal Aspects of Computing | 1996-02-25 | Paper |
| scientific article; zbMATH DE number 4082917 (Why is no real title available?) | 1988-01-01 | Paper |
