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.
展开▼
