NATIONAL INSTITUTE OF AEROSPACE

Contact Us

Colin Britcher, Ph.D.
Director of Graduate Education
757.325.6730
colin.britcher@nianet.org  

Mary Catherine Bunde, M.Ed.
Senior Education Administrator
757.325.6731
mary.bunde@nianet.org

8.11.14 Laurent

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:

  1. The k-induction algorithm, enriched with abstraction and path compression
  2. 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

BUSINESS WITH NIA

Headquarters

100 Exploration Way
Hampton, VA 23666
(757)325-6700
www.nianet.org