An Interaction Concept for Program Verification Systems with Explicit Proof Object

Reviewed Paper In Proceedings

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.

BibTeX

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