ARCHIVE - This is very old!


Input/output verification

By Willem Penninckx, Bart Jacobs, and Frank Piessens

Paper

  • Paper [PDF]: Sound, modular and compositional verification of the input/output behavior of programs
    Willem Penninckx, Bart Jacobs, Frank Piessens. In Proc. ESOP 2015

    Abstract 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.

Other files

  • 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.