Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques
George E. Hagen, Cesare Tinelli · 2008
We present a general approach for verifying safety properties of Lustre 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 implementation of the approach is highly competitive with existing verification solutions for Lustre.