AN INSIGHT INTO SMT-BASED MODEL CHECKING TECHNIQUES FOR FORMAL SOFTWARE VERIFICATION
Jonathan Laurent, NIA Visitor from École Normale Supérieure
August 11, 2014, 10:00 am, NIA, Rm 101
Seminar Video
Abstract:
Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide a partial answer to one of its main issue which is scalabilty. In the context of the formal verification of safety properties on
synchronous dataflow programs, we examine a SMT-based approach which led to the development of the Kind2 model checker and yielded promising experimental results. We give an insight into the two algorithms powering this tool:
- The k-induction algorithm, enriched with abstraction and path compression
- The IC3 algorithm, with approximate quantifier elimination to generalize counterexamples
Bio:
Interpolation and SAT-based Model Checking, K.L. McMillan Scaling up the formal verification of Lustre programs with SMT-based techniques, G. Hagen, C. Tinelli
SMT-based Unbounded Model Checking with IC3 and Approximate Quantifier Elimination [Draft], C. Sticksel, C. Tinelli