Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti
Center for Information Technology, Trento, Italy
Abstract
Model checking invariant properties of designs, represented as transition systems is a fundamental problem in verification. We focus on the practically relevant case where the transition system is expressed with non-linear real arithmetic (NRA). On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA.
In this talk, a counterexample-guided abstraction refinement (CEGAR) approach is presented, that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The approach supports the analysis of polynomials, and is extended to deal with transcendental functions.
The results of an empirical evaluation confirm the validity and potential of this approach.
Short Bio
Alessandro Cimatti is a senior researcher at Fondazione Bruno Kessler, Trento, Italy, where he leads the research unit in Embedded Systems at the Center for Information and Communication Technologies. His research interests concern formal verification of industrial critical systems, methodologies for design and verification of hardware/software systems, decision procedures and their application, safety analysis, diagnosis and diagnosability.
Cimatti has published more than one hundred and thirty papers in the fields of Formal Methods and Artificial Intelligence.
He has co-chaired the FMCAD, SAT and SEFM conferences, and has been member of the Program Committee of the major conferences in computer-aided verification and artificial intelligence.
Cimatti is also interested in the development of software tools for verification (including the MathSAT SMT solver and the nuXmv model checker), and in their application on the field. Cimatti has been the leader of several technology transfer projects in related fields, including projects funded by the European Space Agency and the European Railways Agency.