Tinelli, to make this possible. We thank our PC for their reviewing efforts: (2009)
Wolfgang Ahrendt, Peter Baumgartner, Christian Fermüller, Ulrich Furbach, Bernhard Gramlich, ...
Our field is called automated theorem proving because traditionally it has been concerned with the art of finding proofs automatically. In the beginning, researchers were motivated by the wish to...
Hilbert’s ɛ-Terms in Automated Theorem Proving (2008)
Martin Giese, Wolfgang Ahrendt
Abstract. ɛ-terms, introduced by David Hilbert [8], have the form ɛx.φ, where x is a variable and φ is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but...
Local Organization: Event4 Event Management Preface (2008)
Wolfgang Ahrendt, Peter Baumgartner, Hans De Nivelle
Deduction, in Bremen, Germany. The name automated theorem proving or automated deduction derives from the fact that the field traditionally focused on the art of automatically finding proofs....
CADE-20 Workshop on Disproving- (2008)
Wolfgang Ahrendt, Peter Baumgartner, Hans De Nivelle
deduction derives from the fact that the field traditionally focussed on the art of automatically finding proofs. Initially, researchers were mainly motivated by the wish to build computer systems...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Peterh. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
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...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz
2, Wolfram Menzel 1, and Peter H. Schmitt 1 1
Wolfgang Ahrendt, Bernhard Beckert, Wolfram Menzel
Reif 2, Gerhard Schellhorn 2 and Peter Schmitt 1 1
Veri cation of a Prolog Compiler { First Steps with KIV (2007)
Gerhard Schellhorn, Abt Programmiermethodik, Wolfgang Ahrendt
This paper describes the rst steps of the formal verication of a Prolog compiler with the KIV system. We build upon the mathematical denitions given by Borger and Rosenzweig in [BR95]. There an...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Embedding ASMs into State Transition Diagrams (2007)
Theo Sattler, Wolfgang Ahrendt
This report relates Abstract State Machines (ASMs) with a particular diagram type of UML, the Sate Transition Diagrams (STDs). The principles of translating ASMs into STDs are discussed and...
Hilbert's -terms in Automated Theorem Proving (2007)
Martin Giese, Wolfgang Ahrendt
Abstract. #-terms, introduced by David Hilbert [8], have the form #x.#, where x is a variable and # is a formula. Their syntactical structure is thus similar to that of a quantified formulae, but...
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...
Verification of a Prolog compiler - first steps with KIV. (2007)
Schellhorn, Gerhard, Ahrendt, Wolfgang
This paper describes the first steps of the formal verification of a Prolog compiler with the KIV system. We build upon the mathematical definitions given by Boerger and Rosenzweig in [BR95]. There...
IJCAR'06 Workshop : Disproving'06: Non-Theorems, Non-Validity, Non-Provability (2006)
Ahrendt, Wolfgang, Baumgartner, Peter, De Nivelle, Hans
The volume contains 9 contributed papers.
Computing Finite Models by Reduction to Function-Free Clause Logic (2006)
De Nivelle, Hans, Baumgartner, Peter, Fuchs, Alexander, Tinelli, Cesare, Ahrendt, Wolfgang, Baumgartner, Peter, ...
We propose to reduce model search to a sequence of satisfiability problems made of function-free clause sets, and to apply efficient theorem provers capable of deciding such problems on them. The...
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...
Wolfgang Ahrendt, Andreas Roth, Ralf Sasse
Abstract. This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic...
Wolfgang Ahrendt, Andreas Roth, Ralf Sasse
Abstract. This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic...
OCL Specifications for the Java Card API (2003)
Daniel Larsson, Wojciech Mostowski, Wolfgang Ahrendt
This Master's thesis discusses the development of OCL specifications for Java Card API, and is part of the KeY project. OCL is a specification language, i.e. it is used to express formally the...
The KeY system: Integrating object-oriented design and formal methods (2002)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Elmar Habermalz, Wolfram Menzel, Wojciech Mostowski, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Deductive search for errors in free data type specifications using model generation (2002)
Abstract. The presented approach aims at identifying false conjectures about free data types. Given a specication and a conjecture, the method performs a search for a model of an according counter...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
Embedding ASMs into state transition diagrams (2000)
Sattler, Theo, Ahrendt, Wolfgang
This report relates Abstract State Machines (ASMs) with a particular diagram type of UML, the Sate Transition Diagrams (STDs). The principles of translating ASMs into STDs are discussed and...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
A basis for model computation in free data types (2000)
Abstract. Abstract data types are specied by some equality logic under the assumption of term generatedness. They are called `free', if terms, built only by constructors, are semantically...
A basis for model computation in free data types (2000)
Abstract. Abstract data types, specied by some equality logic under the assumption of term generatedness, are called `free', if terms, built only by constructors, are semantically unique. This...
The KEY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive...
Proof transformations from search-oriented into interaction-oriented tableau calculi (1999)
Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert
Abstract: Logic calculi, and Gentzen-type calculi in particular, can be categorised into two types: search-oriented and interaction-oriented calculi. Both these types have certain...
Proof transformations from search-oriented into interaction-oriented tableau calculi (1999)
Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckerr
Abstract: Logic calculi, and Gentzen-type calculi in particular, can be categorised into two types: search-oriented and interaction-oriented calculi. Both these types have certain inherent...
Integrating automated and interactive theorem proving (1998)
Wolfgang Ahrendt, Bernhard Beckert, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, Peter Schmitt
Abstract. This paper highlights a project to integrate interactive and automated theorem proving in Software Verification. Its aim is to combine the advantages of the two paradigms. We report on the...
Reasoning about abstract state machines: The WAM case study (1997)
Gerhard Schellhorn, Wolfgang Ahrendt
Abstract: This paper describes the rst half of the formal veri cation of a Prolog compiler with the KIV (\Karlsruhe Interactive Veri er") system. Our work is based on [BR95], where an...
Verification of a Prolog Compiler -- First Steps with KIV (1996)
Gerhard Schellhorn, Abt Programmiermethodik, Wolfgang Ahrendt
This paper describes the first steps of the formal verification of a Prolog compiler with the KIV system. We build upon the mathematical definitions given by Borger and Rosenzweig in [BR95]. There an...
Verification of a Prolog Compiler - First Steps with KIV (1996)
Gerhard Schellhorn, Abt Programmiermethodik, Wolfgang Ahrendt
This paper describes the first steps of the formal verification of a Prolog compiler with the KIV system. We build upon the mathematical definitions given by Borger and Rosenzweig in [BR95]. There an...