Seminar: Graduate Seminar
Semantic Simplifications for Improved Verification
Lecturer:
Maayan Astary
Research Areas:
| Model checking is a standard technique for formal verification, and its central obstacle is the state-explosion problem. Classical reductions, such as symmetry, partial-order and cone-of-influence reduction, mitigate this problem by exploiting regularities that manifest syntactically in the design. In practice, however, such syntactic techniques are often insufficient, since in order to simplify a design we need some semantic insight. We propose a scheme for identifying, certifying and exploiting semantic simplifications. A simplification consists of a local criterion, which is checked automatically on the design, and an exploitation function, typically an assumption on the inputs, under which the specification is then verified. The scheme involves proving manually, once, that the criterion allows the exploitation. Such a proof then applies to every design that satisfies the criterion. We instantiate the scheme for a shared linked-list FIFO, and develop an initial lexicon of simplifications, allowing such simplifications as client reduction, data independence, client symmetry and action commutativity. Our experiments show that several of these simplifications significantly reduce verification time, even when the cost of certifying them is included.M.Sc. student under the supervision of Prof. Shaull Almagor.
|