Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking Roberto Cavada, Charle Pecheur
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler Andreas Lochbihler
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation Joachim Breitner