Proof Search with Taclets

Buchkapitel

Autor(en):Philipp Rümmer und Mattias Ulbrich
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Reihe:Lecture Notes in Computer Science
Band:10001
Jahr:2016
Seiten:107-147
URL:http://dx.doi.org/10.1007/978-3-319-49812-6_4
DOI:10.1007/978-3-319-49812-6_4
Links:

Abstract

This chapter covers the formalism of taclets by which inference rules can be formulated for the JavaDL sequent calculus employed in KeY. After an introductory tutorial, the syntax and semantics of the taclet language are described. Finally, techniques are presented to mechanically prove taclet soundness by deriving formulas from taclets whose validity entails the soundness.

BibTeX

@incollection{RummerUlbrich2016,
  author    = {Philipp R{\"{u}}mmer and Mattias Ulbrich},
  title     = {Proof Search with Taclets},
  booktitle = {Deductive Software Verification - The KeY Book: From Theory to Practice},
  pages     = {107--147},
  year      = {2016},
  month     = dec,
  url       = {http://dx.doi.org/10.1007/978-3-319-49812-6_4},
  doi       = {10.1007/978-3-319-49812-6_4},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  publisher = {Springer}
}