(Symbolic) Debugging

The Symbolic Execution Debugger (SED) is a platform for symbolic execution in general and allows to interactively debug programs based on symbolic execution. Symbolic execution discovers all possible execution paths simultaneously. This is achieved by the use of symbolic in lieu of concrete values resulting in a symbolic execution tree. Each node in the symbolic execution tree provides the full state and related information such as the symbolic call stack or the path conditions under which the node is reached.

Execution can start at any method or at any statement without setting up a context. Navigation is realized using classic debugger functionality, including stepwise execution or breakpoints.

Additional information can be found at the old KeY website.

Screencast: Symbolic Execution Debugger (SED)

Literature

2019

Hentschel, Martin; Bubel, Richard; Hähnle, Reiner

The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more Journal Article

In: International Journal on Software Tools for Technology Transfer, 2019, ISSN: 1433-2787.

Abstract | Links | BibTeX

2016

Hentschel, Martin; Hähnle, Reiner; Bubel, Richard

The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Proceedings Article

In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.

Abstract | BibTeX

Hentschel, Martin

Integrating Symbolic Execution, Debugging and Verification PhD Thesis

Technische Universität Darmstadt, 2016.

Abstract | BibTeX

Hentschel, Martin; Hähnle, Reiner; Bubel, Richard

Can Formal Methods Improve the Efficiency of Code Reviews? Proceedings Article

In: Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp. 3–19, 2016.

Links | BibTeX

2014

Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias

The KeY Platform for Verification and Analysis of Java Programs Proceedings Article

In: Giannakopoulou, Dimitra; Kroening, Daniel (Ed.): Verified Software: Theories, Tools, and Experiments (VSTTE 2014), pp. 1–17, Springer-Verlag, 2014, ISBN: 978-3-642-54107-0.

Abstract | Links | BibTeX