Scaling up the formal verification of Lustre programs with SMT-based techniques

We present a general approach for verifying safety properties of Lus-tre programs automatically. Key aspects of the approach are the choice of an expressive first-order logic in which Lustre’s semantics is modeled very naturally, the tailoring to this logic of SAT-based k-induction and abstraction techniques, and the use of SMT solvers to reason efficiently in this logic. We discuss initial experimental results showing that our imple-mentation of the approach is highly competitive with existing verification solutions for Lustre.