Formal Verification Blog

These notes contain examples of formal verification techniques using different formalisms and tools. My goal is to illustrate here nontrivial techniques, emphasizing subtleties I have encountered when using these tools.

These notes are published as a blog, but they will also be used in graduate courses on formal verification I have been teaching at Ecole Normale Supérieure de Rennes and Université de Rennes.

Posts

1. Assume-Guarantee Proofs for SystemVerilog Using SymbioYosys

   Acyclic and circular assume-guarantee rules and their use with the sby tool for proving properties of SystemVerilog modules compositionally.

2. Inductive Invariants in TLA+ using Apalache

   How to formalize a distributed algorithm in TLA+, and proving inductive invariant with Apalache. Symmetry and abstraction techniques to improve scalability.

Contact

You can reach me via my academic homepage.