Institut für Theoretische Informatik (ITI) – Anwendungsorientierte Formale Verifikation

Usability Recommendations for User Guidance in Deductive Program Verification

Book Chapter

Author(s):Sarah Grebing and Mattias Ulbrich
In:Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:12345
Part:IV: Feasibility and Usability
Chapter:11
Year:2020
Pages:261-284
DOI:10.1007/978-3-030-64354-6_11

Abstract

Despite the increasing degree of automation, user input for guiding proof search and construction is still needed in interactive deductive program verification systems, even more so as the size of the investigated programs gets larger and the properties to be verified gain in complexity. We will present recommendations for the design of user interfaces in deductive program verification systems. The goal is to always provide the user with an easy but in depth understanding of the current proof status and guide him towards next expedient interactions. These recommendations are conclusions from a qualitative study with users of the KeY system and from our own experience in using and building different interactive verification systems. We will present the user study together with a summary of the main observations and insights.

BibTeX

@incollection{GrebingUlbrich2020,
  author    = {Sarah Grebing and
               Mattias Ulbrich},
  title     = {Usability Recommendations for User Guidance in
               Deductive Program Verification},
  editor    = {Wolfgang Ahrendt and
               Bernhard Beckert and
               Richard Bubel and
               Reiner H{\"a}hnle and
               Mattias Ulbrich},
  booktitle = {Deductive Software Verification: Future Perspectives - Reflections
               on the Occasion of 20 Years of {\KeY}},
  pages     = {261--284},
  chapter   = {11},
  part      = {IV: Feasibility and Usability},
  year      = {2020},
  month     = dec,
  abstract  = {Despite the increasing degree of automation, user input for
               guiding proof search and construction is still needed in
               interactive deductive program verification systems, even more so
               as the size of the investigated programs gets larger and the
               properties to be verified gain in complexity. We will present
               recommendations for the design of user interfaces in deductive
               program verification systems. The goal is to always provide the
               user with an easy but in depth understanding of the current proof
               status and guide him towards next expedient interactions. These
               recommendations are conclusions from a qualitative study with
               users of the {\KeY} system and from our own experience in using
               and building different interactive verification systems. We will
               present the user study together with a summary of the main
               observations and insights.},
  doi       = {10.1007/978-3-030-64354-6_11},
  series    = {Lecture Notes in Computer Science},
  volume    = {12345},
  publisher = {Springer}
}