Proof Search with Taclets

Book Chapter

Author(s):Philipp Rümmer and Mattias Ulbrich
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Series:Lecture Notes in Computer Science
Volume:10001
Year:2016
Pages: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}
}