Hentschel, Martin ; Hähnle, Reiner ; Bubel, Richard (2016)
An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier.
Singapore, Singapore
doi: 10.1145/2970276.2970303
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2016 |
| Autor(en): | Hentschel, Martin ; Hähnle, Reiner ; Bubel, Richard |
| Art des Eintrags: | Bibliographie |
| Titel: | An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier |
| 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.2970303 |
| Kurzbeschreibung (Abstract): | Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch. |
| Freie Schlagworte: | Verification, Proof Understanding, Empirical Evaluation |
| ID-Nummer: | TUD-CS-2016-1425 |
| 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