Hentschel, Martin ; Hähnle, Reiner ; Bubel, Richard (2016)
The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts.
Singapore, Singapore
doi: 10.1145/2970276.2970292
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2016 |
| Autor(en): | Hentschel, Martin ; Hähnle, Reiner ; Bubel, Richard |
| Art des Eintrags: | Bibliographie |
| Titel: | The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts |
| Sprache: | Deutsch |
| Publikationsjahr: | September 2016 |
| Verlag: | ACM |
| Buchtitel: | Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering |
| Reihe: | ASE 2016 |
| Veranstaltungsort: | Singapore, Singapore |
| DOI: | 10.1145/2970276.2970292 |
| Kurzbeschreibung (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. |
| Freie Schlagworte: | Symbolic Execution, Debugging, Program Execution Visualization, Verification, Proof Understanding |
| ID-Nummer: | TUD-CS-2016-1426 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 03 Jun 2018 21:30 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum