University of Minnesota
Software Engineering Center
/

You are here

Cesare Tinelli

Recent Publications

Incremental Verification with Mode Machine Invariants in State Machines

We describe two complementary techniques to aid the automatic verification of safety properties of synchronous systems by model checking. A first technique allows the automatic generation of certain inductive invariants for mode variables. Such invariants are crucial in the verification of safety properties in systems with complex modal behavior. A second technique allows the simultaneous verification of multiple properties incrementally. Specifically, the outcome of a property—valid or invalid—is communicated to the user as soon as it is known.