Wolfgang Ahrendt

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:

the CADE 2007 Workshop on Disproving, which I organised together with Peter Baumgartner and Hans de Nivelle on July 16, 2007, Bremen, Germany.
the FLoC/IJCAR 2006 Workshop on Disproving, which we organised in Seattle, USA.
the CADE 2005 Workshop on Disproving, which we organised in Tallinn, Estonia.
the IJCAR 2004 Workshop on Disproving, which we organised in Cork, Ireland. That workshop resulted in Decision Procedures and Disproving, a collection of revised selected papers.
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 Ph.D. thesis " Deduktive Fehlersuche ..." (supervised by Reiner Hähnle)

Automated Deduction

Beside my work on disproving conjectures, I worked on the opposite, 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:

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

Formal Methods in Software Engineering

I am involved in the KeY project. The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of the University of Karlsruhe, Chalmers University of Technology, Gothenburg, and the University of Koblenz. Before engaging in KeY, I got in touch with different specification approaches: Rewriting Logic (realised in the Maude system), 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 book, in which I wrote a chapter on "Using KeY"
the KeY page
a recent overview paper on the architecture and philosophy of the KeY tool
a general tutorial paper on specification and verification with the KeY tool
the paper "The KeY Tool", which is right now the best source of information on the KeY project and the KeY tool
a paper about the "Automatic Validation of Transformation Rules ..." from the KeY calculus, employing the Maude system
other papers about KeY: "The KeY Tool", " The KeY Approach: ... ", " The KeY System: ... "
a report about " Embedding ASMs ... " into UML

Before working in the KeY project, I did program verification in the frame of 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

Community Work

I am secretary, and member of the steering committees, of the following two interconnected organisations:

CADE: The Conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974. Previous CADEs were mostly biennial, and annual conferences started in 1996. Since 2001 CADE has participated in the International Joint Conference on Automated Reasoning (IJCAR). CADE Inc. is a subcorporation of the AAR, see below.
AAR: The Association for Automated Reasoning (AAR), is a not-for-profit corporation intended for educational and scientific purposes. The objective of the AAR is to advance the field of automated reasoning by disseminating and exchanging information among its international members on such topics as automated reasoning, automated theorem proving, declarative programming, and automated verification. The major conferences of the AAR comunity are CADE and IJCAR. AAR members are eligible for a substantially reduced subscription rate to the Journal of Automated Reasoning. Membership in the AAR is free, and open to all those interested in automated reasoning. To join the AAR, please contact me.

Workshop organisation:

DISPROVING: I have initiated, co-organised and co-chaired a number of workshops on DISPROVING, see the paragraph on Model Generation and Disproving.

Teaching

Software Engineering using Formal Methods: the course web page
Testing, Debugging, and Verification: the course web page
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

Responsibilities in Education

IT Programme (Engineering Programme in Software Engineering, civilingenjörsprogram Informationsteknik): I am the head of the IT programme, which is a five years engineering programme in Software Engineering at Chalmers University of Technology.
It consists of a Bachelor line, and three Master Programmes: Software Engineering and Technology, Interaction Design, and Intelligent Systems Design.
Computer Science Programme (Datavetenskapligt Program): In the past, I was director of the Computer Science Master/Bachelor Programme (Datavetenskapligt Program) at the University of Gothenburg.
Secure and Dependable Computer Systems (SDCS): In the past, I was director of the Master's Programme in Secure and Dependable Computer Systems at Chalmers University of Technology.

Peer Reviewed Conference and Journal Publications

A Unified Approach for Static and Runtime Verification: Framework and Applications: Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider
Leveraging Applications of Formal Methods, Verification and Validation
5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece
Proceedings, Part I, Springer-Verlag, LNCS 7609.
doi: 10.1007/978-3-642-34026-0_24
Abstract - Bibtex
Real-time Java API specifications for high coverage test generation: Wolfgang Ahrendt, Wojciech Mostowski, Gabriele Paganelli
10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES '12
ACM, 2012
doi: 10.1145/2388936.2388960
Abstract - Bibtex
A System for Compositional Verification of Asynchronous Objects: Wolfgang Ahrendt, Maximilian Dylla
Science of Computer Programming
Elsevier, 2012
doi: 10.1016/j.scico.2010.08.003
Abstract - Bibtex
Practical Aspects of Automated Deduction for Program Verification: Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer
KI - Künstliche Intelligenz
Volume 24, Number 1 / April, 2010, Pages 43-49
Springer Berlin / Heidelberg
Abstract - Bibtex
A Verification System for Distributed Objects with Asynchronous Method Calls: Wolfgang Ahrendt, Maximilian Dylla
Formal Methods and Software Engineering
International Conference on Formal Engineering Methods, ICFEM'09
Rio de Janeiro, Brazil, December 2009
Springer, LNCS 5885.
Abstract - PDF - Bibtex
Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created: Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe
FM 2009: Formal Methods, Second World Congress
Eindhoven, The Netherlands, November 2009
Springer, LNCS 5850.
Abstract - Bibtex
Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification: Wolfgang Ahrendt, Richard Bubel, Reiner Hähnle
Second International Conference on Teaching Formal Methods
Eindhoven, The Netherlands, November 2009
Springer, LNCS 5846.
Abstract - Bibtex
Verifying Object-Oriented Programs with KeY: A Tutorial: Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt
5th International Symposium on Formal Methods for Components and Objects, Amsterdam,
The Netherlands, November 2006
Revised Lectures
Springer, LNCS 4709.
Abstract - PDF - Bibtex
KeY: A Formal Method for Object-Oriented Systems (invited paper): Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS), Paphos, Cyprus, June 2007
Springer, LNCS 4468.
Abstract - PDF - Bibtex
Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics: Wolfgang Ahrendt, Andreas Roth, Ralf Sasse
12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR,
Montego Bay, Jamaica, December 2005
Springer, LNCS 3835.
Abstract - PDF - Bibtex
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

Book Chapter

Using KeY: Wolfgang Ahrendt
chapter in the book:
Verification of Object-Oriented Software:
The KeY Approach
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.)
15 chapters and 2 appendices, xxix + 658 pages
ISBN: 3-540-68977-X
Springer-Verlag, LNCS 4334 - BibTeX - Book Website

Edited Collection

Decision Procedures and Disproving
Selected Papers from the Workshop on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR) 2004: Edited by Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli
Elsevier, ENTCS, volume 125, issue 3, 2005
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: the CADE 2007 Workshop on Disproving, which I organised together with Peter Baumgartner and Hans de Nivelle on July 16, 2007, Bremen, Germany. the FLoC/IJCAR 2006 Workshop on Disproving, which we organised in Seattle, USA. the CADE 2005 Workshop on Disproving, which we organised in Tallinn, Estonia. the IJCAR 2004 Workshop on Disproving, which we organised in Cork, Ireland. That workshop resulted in Decision Procedures and Disproving, a collection of revised selected papers. 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 Ph.D. thesis " Deduktive Fehlersuche ..." (supervised by Reiner Hähnle) Automated Deduction Beside my work on disproving conjectures, I worked on the opposite, 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: papers about automated and interactive theorem proving: " Proof Transformations ... " , " Integrating Automated and Interactive Theorem Proving " a paper about " Hilbert's Epsilon terms ... " 3TAP Formal Methods in Software Engineering I am involved in the KeY project. The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of the University of Karlsruhe, Chalmers University of Technology, Gothenburg, and the University of Koblenz. Before engaging in KeY, I got in touch with different specification approaches: Rewriting Logic (realised in the Maude system), 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 book, in which I wrote a chapter on "Using KeY" the KeY page a recent overview paper on the architecture and philosophy of the KeY tool a general tutorial paper on specification and verification with the KeY tool the paper "The KeY Tool", which is right now the best source of information on the KeY project and the KeY tool a paper about the "Automatic Validation of Transformation Rules ..." from the KeY calculus, employing the Maude system other papers about KeY: "The KeY Tool", " The KeY Approach: ... ", " The KeY System: ... " a report about " Embedding ASMs ... " into UML Before working in the KeY project, I did program verification in the frame of 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
Community Work
I am secretary, and member of the steering committees, of the following two interconnected organisations: CADE The Conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974. Previous CADEs were mostly biennial, and annual conferences started in 1996. Since 2001 CADE has participated in the International Joint Conference on Automated Reasoning (IJCAR). CADE Inc. is a subcorporation of the AAR, see below. AAR The Association for Automated Reasoning (AAR), is a not-for-profit corporation intended for educational and scientific purposes. The objective of the AAR is to advance the field of automated reasoning by disseminating and exchanging information among its international members on such topics as automated reasoning, automated theorem proving, declarative programming, and automated verification. The major conferences of the AAR comunity are CADE and IJCAR. AAR members are eligible for a substantially reduced subscription rate to the Journal of Automated Reasoning. Membership in the AAR is free, and open to all those interested in automated reasoning. To join the AAR, please contact me. Workshop organisation: DISPROVING I have initiated, co-organised and co-chaired a number of workshops on DISPROVING, see the paragraph on Model Generation and Disproving.
Teaching
Software Engineering using Formal Methods the course web page Testing, Debugging, and Verification the course web page 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
Responsibilities in Education
IT Programme (Engineering Programme in Software Engineering, civilingenjörsprogram Informationsteknik) I am the head of the IT programme, which is a five years engineering programme in Software Engineering at Chalmers University of Technology. It consists of a Bachelor line, and three Master Programmes: Software Engineering and Technology, Interaction Design, and Intelligent Systems Design. Computer Science Programme (Datavetenskapligt Program) In the past, I was director of the Computer Science Master/Bachelor Programme (Datavetenskapligt Program) at the University of Gothenburg. Secure and Dependable Computer Systems (SDCS) In the past, I was director of the Master's Programme in Secure and Dependable Computer Systems at Chalmers University of Technology.
Peer Reviewed Conference and Journal Publications
A Unified Approach for Static and Runtime Verification: Framework and Applications Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider Leveraging Applications of Formal Methods, Verification and Validation 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece Proceedings, Part I, Springer-Verlag, LNCS 7609. doi: 10.1007/978-3-642-34026-0_24 Abstract - Bibtex Real-time Java API specifications for high coverage test generation Wolfgang Ahrendt, Wojciech Mostowski, Gabriele Paganelli 10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES '12 ACM, 2012 doi: 10.1145/2388936.2388960 Abstract - Bibtex A System for Compositional Verification of Asynchronous Objects Wolfgang Ahrendt, Maximilian Dylla Science of Computer Programming Elsevier, 2012 doi: 10.1016/j.scico.2010.08.003 Abstract - Bibtex Practical Aspects of Automated Deduction for Program Verification Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer KI - Künstliche Intelligenz Volume 24, Number 1 / April, 2010, Pages 43-49 Springer Berlin / Heidelberg Abstract - Bibtex A Verification System for Distributed Objects with Asynchronous Method Calls Wolfgang Ahrendt, Maximilian Dylla Formal Methods and Software Engineering International Conference on Formal Engineering Methods, ICFEM'09 Rio de Janeiro, Brazil, December 2009 Springer, LNCS 5885. Abstract - PDF - Bibtex Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe FM 2009: Formal Methods, Second World Congress Eindhoven, The Netherlands, November 2009 Springer, LNCS 5850. Abstract - Bibtex Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification Wolfgang Ahrendt, Richard Bubel, Reiner Hähnle Second International Conference on Teaching Formal Methods Eindhoven, The Netherlands, November 2009 Springer, LNCS 5846. Abstract - Bibtex Verifying Object-Oriented Programs with KeY: A Tutorial Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt 5th International Symposium on Formal Methods for Components and Objects, Amsterdam, The Netherlands, November 2006 Revised Lectures Springer, LNCS 4709. Abstract - PDF - Bibtex KeY: A Formal Method for Object-Oriented Systems (invited paper) Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS), Paphos, Cyprus, June 2007 Springer, LNCS 4468. Abstract - PDF - Bibtex Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics Wolfgang Ahrendt, Andreas Roth, Ralf Sasse 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, Montego Bay, Jamaica, December 2005 Springer, LNCS 3835. Abstract - PDF - Bibtex 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
Book Chapter
Using KeY Wolfgang Ahrendt chapter in the book: Verification of Object-Oriented Software: The KeY Approach Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.) 15 chapters and 2 appendices, xxix + 658 pages ISBN: 3-540-68977-X Springer-Verlag, LNCS 4334 - BibTeX - Book Website
Edited Collection
Decision Procedures and Disproving Selected Papers from the Workshop on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR) 2004 Edited by Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli Elsevier, ENTCS, volume 125, issue 3, 2005 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