A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela + (2008)
Florian Rabe, Steffen Schlager, Peter H. Schmitt
Abstract. In this paper we introduce the first-order dynamic logic DLP for Promela +, a language subsuming the modelling language Promela of the Spin model checker. In DLP trace modalities can be...
A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela + (2008)
Florian Rabe, Steffen Schlager, Peter H. Schmitt
Abstract. We introduce the first-order dynamic logic DLP for Promela +, a language subsuming the modelling language Promela of the Spin model checker. In DLP trace modalities can be used to reason...
Bernhard Beckert, Steffen Schlager
Abstract. Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to...
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2008)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
Bernhard Beckert, Steffen Schlager
Abstract. Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to...
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...
Bernhard Beckert, Vladimir Klebanov, Steffen Schlager
In the previous chapter, we have introduced a variant of classical predicate logic that has a rich type system and a sequent calculus for that logic. This predicate logic can easily be used to...
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...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2007)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
An improved rule for while loops in deductive program verification (2005)
Beckert, Bernhard, Schlager, Steffen, Schmitt, Peter H.
The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual pre-/post-condition pairs...
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...
An improved rule for while loops in deductive program verification (2005)
Bernhard Beckert, Steffen Schlager, Peter H. Schmitt
Abstract. The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2004)
Bernhard Beckert, Bernhard Beckert, Martin Giese, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
Abstract. Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing...
In Formal Methods for Open Object-Based Distributed Systems (2004)
Abb Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
[AdB90] Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2):129– 162, 1990. [AdB94] Pierre America and Frank de Boer. Reasoning...
Software verification with integrated data type refinement for integer arithmetic (2004)
Bernhard Beckert, Steffen Schlager
Abstract. We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into...
Software verification with integrated data type refinement for integer arithmetic (2004)
Bernhard Beckert, Steffen Schlager
Abstract. We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into...