Symbolic Execution with CEGAR

Beyer, Dirk and Lemberger, Thomas (2016): Symbolic Execution with CEGAR. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. Lecture Notes in Computer Science, Vol. 9952. Cham: Springer. pp. 195-211

Abstract

Symbolic execution, a standard technique in program analysis, is a particularly successful and popular component in systems for test-case generation. One of the open research problems is that the approach suffers from the path-explosion problem. We apply abstraction to symbolic execution, and refine the abstract model using counterexample-guided abstraction refinement (CEGAR), a standard technique from model checking. We also use refinement selection with existing and new heuristics to influence the behavior and further improve the performance of our refinement procedure. We implemented our new technique in the open-source software-verification framework CPACHEKARexperimental results show that the implementation is highly competitive.

• Item Type: Book Section
• Faculties: Mathematics, Computer Science and Statistics > Computer Science
• Subjects: 000 Computer science, information and general works > 004 Data processing computer science
• ISBN: 978-3-319-47165-5; 978-3-319-47166-2
• ISSN: 0302-9743
• Place of Publication: Cham
• Language: English