Coq formalization and soundness proof for an input/output verification approach
Willem Penninckx, Bart Jacobs · Zenodo (CERN European Organization for Nuclear Research) · 2016
This is a 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 used: 8.4pl4