Unilogo Unilogo
[Picture of Wolfgang Ahrendt]

Wolfgang Ahrendt

Associate Professor
Communication Services:
Phone: +46-31-772-1011
Fax: +46-31-772-3663
Email: ahrendt@chalmers.se
Room 5477
EDIT-building, at Rännvägen 6B
Department of Computer Science and Engineering
Chalmers University of Technology
SE-41296 Göteborg
Fields of Work and Interest
[Top of Page]

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.

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.

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.
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).

Community Work
[Top of Page]

I am secretary, and member of the steering committees, of the following two interconnected organisations:
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.

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:
I have initiated, co-organised and co-chaired a number of workshops on DISPROVING, see the paragraph on Model Generation and Disproving.
[Top of Page]

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
[Top of Page]

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
[Top of Page]

A Specification Language for Static and Runtime Verification of Data and Control Properties
Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider
FM 2015, 20th International Symposium on Formal Methods
Oslo, Norway, June 2015
Springer, LNCS, to appear.
Abstract - Pre-print - Bibtex

Integrating Deductive Verification and Symbolic Execution for Abstract Object Creation in Dynamic Logic
Stijn de Gouw, Frank de Boer, Wolfgang Ahrendt, Richard Bubel
Software and Systems Modeling, 2015 (to appear)
Abstract - Bibtex

The KeY Platform for Verification and Analysis of Java Programs
Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns , Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich
Verified Software: Theories, Tools and Experiments 2014, 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers, Springer-Verlag, LNCS 8471.
doi: 10.1007/978-3-319-12154-3
Abstract - Bibtex

Verifying (in-)stability in floating-point programs by increasing precision using SMT solvers
Gabriele Paganelli, Wolfgang Ahrendt
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2013)
Abstract - Bibtex

Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks
Stijn de Gouw, Frank de Boer, Wolfgang Ahrendt, Richard Bubel
39th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2013), Špindlerův Mlýn, Czech Republic, January 26-31, 2013. Proceedings, Springer-Verlag, LNCS 7741.
doi: 10.1007/978-3-642-35843-2_19
Abstract - Bibtex

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 - PDF - 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
[Top of Page]

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
[Top of Page]

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

Other papers and reports
[Top of Page]

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

[Top of Page]

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