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

An Interaction Concept for Program Verification Systems with Explicit Proof Object

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert, Sarah Grebing und Mattias Ulbrich
In:Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10629
Jahr:2017
Seiten: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}
}