Sciweavers

Share
FMCAD
2008
Springer

Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques

12 years 1 months ago
Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques
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 ion 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.
George Hagen, Cesare Tinelli
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FMCAD
Authors George Hagen, Cesare Tinelli
Comments (0)
books