Paper [PDF]: Sound, modular and compositional verification of the input/output behavior of programsAbstract We present a sound verification approach for verifying input/output properties of programs. Our approach supports defining high-level I/O actions on top of low-level ones (compositionality), defining input/output actions without taking into account which other actions exist (modularity), and other features. As the key ingredient, we developed a separation logic over Petri nets. We also show how with the same specification style we can elegantly modularly verify “I/O-like” code that uses the Template Pattern. We have implemented our approach in the VeriFast verifier and applied it to a number of challenging examples.
Willem Penninckx, Bart Jacobs, Frank Piessens. In Proc. ESOP 2015
- Slides [PDF]: I/O verification: formalization and soundness proof. DRADS 2017.
- Coq files [.tar.xz] (mirror) (DOI): Coq formalization and soundness proof for an input/output verification approach. The proof rules do not support verifying nonterminating executions, although the step semantics support nonterminating runs. Coq version: 8.4pl4. Date: 2016.
Slides [PDF]: Presentation for ESOP 2015.
- Slides [PDF]: Presentation for DRADS 2014