Specification Predicates with Explicit Dependency Information (2009)
Richard Bubel, Reiner Hähnle, Peter H. Schmitt
Abstract. Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive...
Abstract Hoare Logic with Updates A Hoare-Style Calculus with Explicit State Updates (2008)
We present a verification system for a variant of Hoare-logic that supports proving program correctness by forward symbolic execution. No explicit weakening rules are needed and first-order reasoning...
The interactive theorem prover developed in the KeY project, which implements a sequent calculus for JavaCard Dynamic Logic (JavaCardDL) is based on taclets. Taclets are lightweight tactics with easy...
Abstract A Hoare-Style Calculus with Explicit State Updates (2008)
We present a verification system for a variant of Hoare-logic that supports proving by forward symbolic execution. In addition, no explicit weakening rules are needed and first-order reasoning is...
Study Key System, Richard Bubel, Reiner Hähnle
The date of receipt and acceptance will be inserted by the editor Abstract. The KeY system allows integrated informal and formal development of object-oriented JAVA software. In this paper we report...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for...
The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for...
The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for...