TU Darmstadt / ULB / TUbiblio

The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts

Hentschel, Martin and Hähnle, Reiner and Bubel, Richard (2016):
The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts.
In: ASE 2016, In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ACM, Singapore, Singapore, pp. 846--851, ISBN 978-1-4503-3845-5,
DOI: 10.1145/2970276.2970292,
[Conference or Workshop Item]

Abstract

The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.

Item Type: Conference or Workshop Item
Erschienen: 2016
Creators: Hentschel, Martin and Hähnle, Reiner and Bubel, Richard
Title: The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts
Language: German
Abstract:

The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.

Title of Book: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering
Series Name: ASE 2016
Publisher: ACM
ISBN: 978-1-4503-3845-5
Uncontrolled Keywords: Symbolic Execution, Debugging, Program Execution Visualization, Verification, Proof Understanding
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Event Location: Singapore, Singapore
Date Deposited: 31 Dec 2016 10:40
DOI: 10.1145/2970276.2970292
Identification Number: TUD-CS-2016-1426
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item