Proof Rules for Model Checking Systems with Data

Abstract

Model checking is an automated technique for verifying temporal properties of finite-state systems. The technique can be used, for example, to verify the finite control parts of computer hardware designs and communication protocols. However, because it requires exhaustively searching the state space of a system to be verified, it cannot generally be applied directly to systems manipulating data, even if the data types are finite. For unbounded or uninterpreted data types, the model checking problem becomes undecidable.

Nonetheless, reductions akin to “program slicing” can be used to reduce the verification of large systems with unbounded data to model checking problems over tractably small models with finite data types. Such a reduction can be obtained, for example, by enumerating the possible paths of a data item through a system. Symmetry can then be exploited to reduce the cases to a tractable number. Use of model checking in this way can greatly simplify proofs by eliminating the need for global invariants.

This talk will show how a system of three inference rules – circular assume/guarantee, temporal case splitting, and symmetry reduction – can be used in conjunction with model checking to yield quite concise proofs of systems that manipulate data.