Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
SMT-Based Software Model Checking
verfasst von : Alessandro Cimatti
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.