### Skapa referens, olika format (klipp och klistra)

**Harvard**

Ahrendt, W. och Grebing, S. (2016) *Using the KeY Prover*.

** BibTeX **

@inbook{

Ahrendt2016,

author={Ahrendt, Wolfgang and Grebing, Sarah},

title={Using the KeY Prover},

booktitle={Deductive Software Verification - The KeY Book},

isbn={978-3-319-49811-9},

pages={495-539},

abstract={This chapter is a self-contained introduction into the usage of the KeY prover, a tool for proving formulas of a program logic called Java Dynamic Logic. It does not assume the reader to have read any other chapter of the book in advance. Here, we discuss the usage of the KeY prover in isolation. For a tutorial on the most common context of the prover, i.e., the KeY verification process, we refer to the chapter `Formal Verification with KeY: A Tutorial'. The present chapter takes entirely the user's perspective on the KeY prover, and the GUI plays an important role. However, we do not only introduce the various ways of using, and interacting with, the KeY prover. Rather, the various visible artifacts the prover acts on, in particular the logic and the taclet language, are introduced on the side, on demand, and example driven, in a light-weight manner. This chapter is meant to be read with the KeY system up and running, such that every step can be tried out immediately in the system. The concepts that will be introduced along with the usage of the prover include KeY problem files, propositional, first-order, and dynamic logic, sequent calculus, proof construction, proof navigation and manipulation, taclets, interactive and automated proving, quantifier instantiation, and symbolic execution. Most of these topics are discussed in much greater detail in other chapters within this book, but appear here in the context of using the KeY prover.
},

year={2016},

keywords={Software Verification, Solftware Analysis, Interactive Theorem Proving},

}

** RefWorks **

RT Book, Section

SR Electronic

ID 246671

A1 Ahrendt, Wolfgang

A1 Grebing, Sarah

T1 Using the KeY Prover

YR 2016

T2 Deductive Software Verification - The KeY Book

SN 978-3-319-49811-9

SP 495

OP 539

AB This chapter is a self-contained introduction into the usage of the KeY prover, a tool for proving formulas of a program logic called Java Dynamic Logic. It does not assume the reader to have read any other chapter of the book in advance. Here, we discuss the usage of the KeY prover in isolation. For a tutorial on the most common context of the prover, i.e., the KeY verification process, we refer to the chapter `Formal Verification with KeY: A Tutorial'. The present chapter takes entirely the user's perspective on the KeY prover, and the GUI plays an important role. However, we do not only introduce the various ways of using, and interacting with, the KeY prover. Rather, the various visible artifacts the prover acts on, in particular the logic and the taclet language, are introduced on the side, on demand, and example driven, in a light-weight manner. This chapter is meant to be read with the KeY system up and running, such that every step can be tried out immediately in the system. The concepts that will be introduced along with the usage of the prover include KeY problem files, propositional, first-order, and dynamic logic, sequent calculus, proof construction, proof navigation and manipulation, taclets, interactive and automated proving, quantifier instantiation, and symbolic execution. Most of these topics are discussed in much greater detail in other chapters within this book, but appear here in the context of using the KeY prover.

LA eng

DO 10.1007/978-3-319-49812-6_15

LK http://dx.doi.org/10.1007/978-3-319-49812-6_15

OL 30