Advertisement
Published in:
2010 | OriginalPaper | Chapter
SMT-Based Software Model Checking
Author : Alessandro Cimatti
Published in: Model Checking Software
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Formal verification is paramount in the development of high-assurance software. Model checking techniques for
sequential
software combine a high degree of automation and the ability to provide conclusive answers, even for infinite state systems. A key paradigm for scalable software model checking is counter-example guided abstraction refinement (CEGAR) [1]. In this paradigm, an abstraction (or over-approximation) of the program is searched for an abstract path leading to an assertion violation. If such a path does not exist, then the program is safe. When such a path exists, and is feasible in the concrete program, then the path is a counter-example witnessing the assertion violation. If the path is infeasible in the concrete program, it is then analyzed to extract information needed to refine the abstraction.