Fields of Work and Interest

Model generation and disproving

I worked on the generation of models for (first order) abstract data types. The goal is to disprove conjectures by generating a model which, while satisfying the axioms of the data type, falsifies the conjecture.
See:

register to the CADE 2005 Workshop on Disproving, which I organise together with Peter Baumgartner and Hans de Nivelle on July 22, 2005, Tallinn, Estonia.
the IJCAR 2004 Workshop on Disproving, organised by the same people, which took place on July 4, 2004.
my paper " Deductive Search for Errors ... ", published at the CADE-18 conference
my paper " A Basis for Model Computation ... " at the CADE-17 workshop on Model Computation
my dissertation thesis " Deduktive Fehlersuche ..." (supervised by Reiner Hähnle)
the world wide Model Computation Page

Automated deduction

Beside my work on disproving conjectures, I worked in the field of the opposite, which is automated theorem proving. In the context of the tableau prover 3TAP and the KIV system, we investigated the combination of automated and interactive theorem proving. The gap between the different calculi used for both styles of proving also motivated our investigation of `epsilon terms' for free variable tableaux.
See:

published papers about automated and interactive theorem proving:
" Proof Transformations ... " , " Integrating Automated and Interactive Theorem Proving "
a published paper about " Hilbert's Epsilon terms ... "
3TAP

Formal methods in software engineering

I am involved in the KeY project. The aim of KeY is to integrate formal software specification and verification into the UML based process of object oriented software development. The tool we are developing is an extension of a commercial case tool and will support formal software development from the instantiation of design patterns down to the verification of Java code.
Before engaging in KeY, I got in touch with different specification approaches: algebraic specification (used in the KIV system), Abstract State Machines (ASMs) and the B method. We also considered the integration of ASMs into UML.
See:

the KeY page
the paper The KeY Tool, which is right now the best source of information on the KeY project and the KeY tool
Other papers about KeY: " The KeY Approach: ... "and" The KeY System: ... "
a report about " Embedding ASMs ... " into UML

Software verification

Before working in the KeY project, I verified programs with the KIV system, by interactively proving theorems in dynamic logic. In particular, I worked on a case study about Prolog compiler verification (based on an ASM specification).
See:

published papers about the compiler verification case study:
" Reasoning about ASMs: ... " , " The WAM Case Study: ... "
my diploma thesis " Von PROLOG zur WAM, Verifikation ..."
KIV

Teaching

Object-oriented programming, advanced course, IT programme: the course web page
First Year Project Course, IT programme: the course web page
Graduate Course: Algebraic Specification of Abstract Data Types: the course web page
D3 Project Proposal: A Literate Programming System

Refereed conference and journal publications

The KeY Tool: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle,
Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt
Software and Systems Modeling, volume 4, number 1, Springer, 2005
Abstract - Bibtex
Deductive Search for Errors in Free Data Type Specifications using Model Generation: Wolfgang Ahrendt
Automated Deduction -- CADE-18, 18th International Conference on Automated Deduction
Copenhagen, Denmark, July 2002
Springer, LNCS 2392.
Abstract - Postscript - Bibtex
The KeY System: Integrating Object-Oriented Design and Formal Methods: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese,
Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Peter H. Schmitt
Fundamental Approaches to Software Engineering. 5th International Conference, FASE 2002.
Held as Part of ETAPS 2002, Grenoble, France, April 2002, Proceedings.
Springer, LNCS 2306.
Abstract - PDF - Appendix - BibTeX
The KeY Approach: Integrating Object Oriented Design and Formal Verification: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese,
Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt
Proceedings, 8th European Workshop on Logics in AI (JELIA), Malaga, Spain, September 2000
Springer, LNCS 1919.
Abstract - PostScript - PDF - BibTeX
Hilbert's Epsilon terms in Automated Theorem Proving: Martin Giese, Wolfgang Ahrendt
Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods
Saratoga Springs, NY, USA, June 1999
Springer, LNCS 1617.
Abstract - Postscript - PDF - Bibtex
Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi: Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert
Journal of Universal Computer Science (J.UCS), vol. 5, issue 3: 113-134, Springer, 1999.
Abstract - Postscript - PDF - Bibtex
Integrating Automated and Interactive Theorem Proving: Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel,
Wolfgang Reif, Gerhard Schellhorn, Peter H. Schmitt
In: W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications.
Volume II: Systems and Implementation Techniques
Kluwer Academic Publishers, Dordrecht, 1998.
Abstract - Postscript - PDF - Bibtex
The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV: Gerhard Schellhorn, Wolfgang Ahrendt
In: W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications.
Volume III: Applications
Kluwer Academic Publishers, Dordrecht, 1998.
Abstract - Postscript - PDF - Bibtex
Reasoning about Abstract State Machines: The WAM Case Study: Gerhard Schellhorn, Wolfgang Ahrendt
Journal of Universal Computer Science (J.UCS), vol. 3, issue 4: 377-413, Springer 1997.
Abstract - Postscript - PDF - Bibtex

Other papers and reports

A Basis for Model Computation in Free Data Types: Wolfgang Ahrendt
Proceedings, CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications.
Pittsburgh, Pennsylvania, USA, 2000.
Abstract - Postscript - PDF - Bibtex
Embedding ASMs into State Transition Diagrams: Theo Sattler, Wolfgang Ahrendt
Technical Report 2000/20, University of Karlsruhe, Department of Computer Science, 2000.
PostScript, PDF, plain text, and graphical version - Bibtex

Theses

Deduktive Fehlersuche in Abstrakten Datentypen: Wolfgang Ahrendt
Dissertation (in German), University of Karlsruhe, Department of Computer Science, July 2001
published online by: Universitätsbibliothek Karlsruhe - Bibtex
Von PROLOG zur WAM, Verifikation der Prozedurübersetzung mit KIV: Wolfgang Ahrendt
Diplomarbeit (in German), University of Karlsruhe, Department of Computer Science, December 1995
Postscript - PDF - Bibtex

Fields of Work and Interest
Model generation and disproving I worked on the generation of models for (first order) abstract data types. The goal is to disprove conjectures by generating a model which, while satisfying the axioms of the data type, falsifies the conjecture. See: register to the CADE 2005 Workshop on Disproving, which I organise together with Peter Baumgartner and Hans de Nivelle on July 22, 2005, Tallinn, Estonia. the IJCAR 2004 Workshop on Disproving, organised by the same people, which took place on July 4, 2004. my paper " Deductive Search for Errors ... ", published at the CADE-18 conference my paper " A Basis for Model Computation ... " at the CADE-17 workshop on Model Computation my dissertation thesis " Deduktive Fehlersuche ..." (supervised by Reiner Hähnle) the world wide Model Computation Page Automated deduction Beside my work on disproving conjectures, I worked in the field of the opposite, which is automated theorem proving. In the context of the tableau prover 3TAP and the KIV system, we investigated the combination of automated and interactive theorem proving. The gap between the different calculi used for both styles of proving also motivated our investigation of `epsilon terms' for free variable tableaux. See: published papers about automated and interactive theorem proving: " Proof Transformations ... " , " Integrating Automated and Interactive Theorem Proving " a published paper about " Hilbert's Epsilon terms ... " 3TAP Formal methods in software engineering I am involved in the KeY project. The aim of KeY is to integrate formal software specification and verification into the UML based process of object oriented software development. The tool we are developing is an extension of a commercial case tool and will support formal software development from the instantiation of design patterns down to the verification of Java code. Before engaging in KeY, I got in touch with different specification approaches: algebraic specification (used in the KIV system), Abstract State Machines (ASMs) and the B method. We also considered the integration of ASMs into UML. See: the KeY page the paper The KeY Tool, which is right now the best source of information on the KeY project and the KeY tool Other papers about KeY: " The KeY Approach: ... "and" The KeY System: ... " a report about " Embedding ASMs ... " into UML Software verification Before working in the KeY project, I verified programs with the KIV system, by interactively proving theorems in dynamic logic. In particular, I worked on a case study about Prolog compiler verification (based on an ASM specification). See: published papers about the compiler verification case study: " Reasoning about ASMs: ... " , " The WAM Case Study: ... " my diploma thesis " Von PROLOG zur WAM, Verifikation ..." KIV
Teaching
Object-oriented programming, advanced course, IT programme the course web page First Year Project Course, IT programme the course web page Graduate Course: Algebraic Specification of Abstract Data Types the course web page D3 Project Proposal A Literate Programming System
Refereed conference and journal publications
The KeY Tool Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt Software and Systems Modeling, volume 4, number 1, Springer, 2005 Abstract - Bibtex Deductive Search for Errors in Free Data Type Specifications using Model Generation Wolfgang Ahrendt Automated Deduction -- CADE-18, 18th International Conference on Automated Deduction Copenhagen, Denmark, July 2002 Springer, LNCS 2392. Abstract - Postscript - Bibtex The KeY System: Integrating Object-Oriented Design and Formal Methods Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Peter H. Schmitt Fundamental Approaches to Software Engineering. 5th International Conference, FASE 2002. Held as Part of ETAPS 2002, Grenoble, France, April 2002, Proceedings. Springer, LNCS 2306. Abstract - PDF - Appendix - BibTeX The KeY Approach: Integrating Object Oriented Design and Formal Verification Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt Proceedings, 8th European Workshop on Logics in AI (JELIA), Malaga, Spain, September 2000 Springer, LNCS 1919. Abstract - PostScript - PDF - BibTeX Hilbert's Epsilon terms in Automated Theorem Proving Martin Giese, Wolfgang Ahrendt Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods Saratoga Springs, NY, USA, June 1999 Springer, LNCS 1617. Abstract - Postscript - PDF - Bibtex Proof Transformations from Search-oriented into Interaction-oriented Tableau Calculi Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert Journal of Universal Computer Science (J.UCS), vol. 5, issue 3: 113-134, Springer, 1999. Abstract - Postscript - PDF - Bibtex Integrating Automated and Interactive Theorem Proving Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, Peter H. Schmitt In: W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume II: Systems and Implementation Techniques Kluwer Academic Publishers, Dordrecht, 1998. Abstract - Postscript - PDF - Bibtex The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV Gerhard Schellhorn, Wolfgang Ahrendt In: W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume III: Applications Kluwer Academic Publishers, Dordrecht, 1998. Abstract - Postscript - PDF - Bibtex Reasoning about Abstract State Machines: The WAM Case Study Gerhard Schellhorn, Wolfgang Ahrendt Journal of Universal Computer Science (J.UCS), vol. 3, issue 4: 377-413, Springer 1997. Abstract - Postscript - PDF - Bibtex
Other papers and reports
A Basis for Model Computation in Free Data Types Wolfgang Ahrendt Proceedings, CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications. Pittsburgh, Pennsylvania, USA, 2000. Abstract - Postscript - PDF - Bibtex Embedding ASMs into State Transition Diagrams Theo Sattler, Wolfgang Ahrendt Technical Report 2000/20, University of Karlsruhe, Department of Computer Science, 2000. PostScript, PDF, plain text, and graphical version - Bibtex
Theses
Deduktive Fehlersuche in Abstrakten Datentypen Wolfgang Ahrendt Dissertation (in German), University of Karlsruhe, Department of Computer Science, July 2001 published online by: Universitätsbibliothek Karlsruhe - Bibtex Von PROLOG zur WAM, Verifikation der Prozedurübersetzung mit KIV Wolfgang Ahrendt Diplomarbeit (in German), University of Karlsruhe, Department of Computer Science, December 1995 Postscript - PDF - Bibtex

Wolfgang Ahrendt