@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},
chapter = {4},
part = {I: Foundations},
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}
}
Proof Search with Taclets
| Author(s): | Philipp Rümmer and Mattias Ulbrich |
|---|---|
| In: | Deductive Software Verification - The KeY Book: From Theory to Practice |
| Publisher: | Springer |
| Series: | Lecture Notes in Computer Science |
| Volume: | 10001 |
| Part: | I: Foundations |
| Chapter: | 4 |
| 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: | Book |
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.