Deductive program verification has made considerable progress in recent years. Automation is the goal, but it is apparent that there will always be challenges that cannot be verified fully automatically, but require some form of user input. We present a novel user interaction concept that allows the user to interact with the verification system on different abstraction levels and on different verification/proof artifacts. The elements of the concept are based on the findings of qualitative user studies we conducted amongst users of interactive deductive program verification systems. Moreover, the concept implements state-of-the-art user interaction principles. We prototypically implemented our concept as an interactive verification tool for Dafny programs.
CITATION STYLE
Grebing, S., Klamroth, J., & Ulbrich, M. (2020). Seamless interactive program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12031 LNCS, pp. 68–86). Springer. https://doi.org/10.1007/978-3-030-41600-3_6
Mendeley helps you to discover research relevant for your work.