TU Darmstadt / ULB / TUbiblio

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

Hentschel, Martin and Hähnle, Reiner and Bubel, Richard (2016):
An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier.
In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ACM, Singapore, Singapore, In: ASE 2016, ISBN 978-1-4503-3845-5,
DOI: 10.1145/2970276.2970303, [Conference or Workshop Item]

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 and Hähnle, Reiner and Bubel, Richard
Title: An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier
Language: German
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.

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: Verification, Proof Understanding, Empirical Evaluation
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.2970303
Identification Number: TUD-CS-2016-1425
Export:

Optionen (nur für Redakteure)

View Item View Item