TU Darmstadt / ULB / TUbiblio

An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier

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 Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen