Usability Recommendations for User Guidance in Deductive Program Verification

@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}
}