@InProceedings{BeckertGrebingUlbrich2017, author = {Bernhard Beckert and Sarah Grebing and Mattias Ulbrich}, title = {An Interaction Concept for Program Verification Systems with Explicit Proof Object}, booktitle = {Hardware and Software: Verification and Testing - 13th Haifa Verification Conference ({HVC} 2017)}, year = {2017}, month = nov, publisher = {Springer}, address = {Cham}, series = {Lecture Notes in Computer Science}, volume = {10629}, pages = {163--178}, doi = {10.1007/978-3-319-70389-3_11}, isbn = {978-3-319-70389-3} }
An Interaction Concept for Program Verification Systems with Explicit Proof Object
Author(s): | Bernhard Beckert, Sarah Grebing, and Mattias Ulbrich |
---|---|
In: | Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017) |
Publisher: | Springer |
Series: | Lecture Notes in Computer Science |
Volume: | 10629 |
Year: | 2017 |
Pages: | 163-178 |
DOI: | 10.1007/978-3-319-70389-3_11 |
Abstract
Deductive program verification is a difficult task: in general, user guidance is required to control the proof search and construction. Providing the right guiding information is challenging for users and usually requires several reiterations. Supporting the user in this process can considerably reduce the effort of program verification.