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
Conference or Workshop Item, Bibliographie
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.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 2016 |
| Creators: | Hentschel, Martin ; Hähnle, Reiner ; Bubel, Richard |
| Type of entry: | Bibliographie |
| Title: | An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier |
| Language: | German |
| Date: | September 2016 |
| Publisher: | ACM |
| Book Title: | Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering |
| Series: | ASE 2016 |
| Event Location: | Singapore, Singapore |
| DOI: | 10.1145/2970276.2970303 |
| 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. |
| Uncontrolled Keywords: | Verification, Proof Understanding, Empirical Evaluation |
| Identification Number: | TUD-CS-2016-1425 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 03 Jun 2018 21:30 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum