Logo Logo
Help
Contact
Switch Language to German
Beyer, Dirk; 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
Full text not available from 'Open Access LMU'.

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.