Home Hector-Kurs Lehre CV Publications Scientific Activities Bauprojekt

Publications

2007

Symbolic Execution as a Framework for Deductive Verification of Object-Oriented Programs
Steffen Schlager
PhD-Thesis, Universität Karlsruhe
Sierke-Verlag

The KeY System 1.0 (Deduction Component)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
Proceedings, International Conference on Automated Deduction (CADE)
PDF - BibTeX - Abstract - Springer-Verlag, LNCS 4603

Dynamic Logic
Bernhard Beckert, Vladimir Klebanov, Steffen Schlager
Chapter 3 in "Verification of Object-Oriented Software - The KeY Approach",
Editors: Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
PDF - BibTeX - Springer-Verlag, LNCS 4334

Java Integers
Steffen Schlager
Chapter 12 in "Verification of Object-Oriented Software - The KeY Approach",
Editors: Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
PDF - BibTeX - Springer-Verlag, LNCS 4334

2005

Verification of JCSP Programs
Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
Proceedings, "Communicating Process Architectures 2005",
Concurrent Systems Engineering Series, Volume 63, pp. 203-218, IOS Press
PDF - BibTeX - Abstract

A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela+
Florian Rabe, Steffen Schlager, and Peter H. Schmitt
Proceedings, "The 17th Nordic Workshop on Programming Theory", Copenhagen, Denmark
PDF - BibTeX - Abstract

An Improved Rule for While Loops in Deductive Program Verification
Bernhard Beckert, Steffen Schlager, and Peter H. Schmitt
7th International Conference on Formal Engineering Methods, Manchester, UK
PDF - BibTeX - Abstract - Springer Verlag, LNCS 3785

A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela+
Florian Rabe, Steffen Schlager, and Peter H. Schmitt
Short Paper Proceedings, "12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning", Montego Bay, Jamaica
PDF - BibTeX - Abstract

Refinement and Retrenchment for Programming Language Data Types
Bernhard Beckert and Steffen Schlager
"Formal Aspects of Computing"
PDF - BibTeX - Abstract - Formal Aspects of Computing (Springer Journal)

An Improved Rule for While Loops in Deductive Program Verification
Bernhard Beckert, Steffen Schlager, and Peter H. Schmitt
Technical Report, Universität Karlsruhe, Faculty for Computer Science
Postscript - BibTeX - Abstract

The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt
Software and System Modeling, © Springer-Verlag
PDF - BibTeX - Abstract - Springer-Online

2004

Software Verification with Integrated Data Type Refinement for Integer Arithmetic
Bernhard Beckert and Steffen Schlager
Proceedings, Fourth International Conference on Integrated Formal Methods, Canterbury, England
PDF - BibTeX - Abstract - Springer Verlag, LNCS 2083

Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager
Revista de la Real Academia de Ciencias (RACSAM)
PDF - BibTeX - Abstract

Supporting Confidentiality in UML: A Profile for the Decentralized Label Model
Jakob Bende, Rogardt Heldal, and Steffen Schlager
3rd International Workshop on Critical Systems Development with UML,Lisbon, Portugal
PDF - BibTeX - Abstract

2003

The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt
Department of Computing Science, Chalmers University and Göteborg University
Technical Report in Computing Science No. 2003-5, February 2003.
PDF - BibTeX - Abstract

2002

Integer Arithmetic in the Specification and Verification of Java Programs
Bernhard Beckert and Steffen Schlager
5th Workshop on Tools for System Design and Verification, Günzburg, Germany
PostScript - BibTeX - Abstract

Handling of Integer Arithmetic in the Verification of Java Programs
Steffen Schlager
Diploma Thesis, University of Karlsruhe, Department of Logic, Complexity, and Deduction Systems
Postscript - BibTeX

2001

A Sequent Calculus for First-order Dynamic Logic with Trace Modalities
Bernhard Beckert and Steffen Schlager
Proceedings, International Joint Conference on Automated Reasoning
PDF - BibTeX - Abstract - Springer Verlag, LNCS 2083

2000

Erweiterung der Dynamischen Logik um temporallogische Operatoren
Steffen Schlager
Studienarbeit, University of Karlsruhe, Department of Logic, Complexity, and Deduction Systems
In German
Postscript - BibTeX

1999

Neue Ansätze zur (weiträumigen) Verteilung in vernetzten Systemen
Steffen Schlager
Internal Report, University of Karlsruhe, Department of Telematics
PDF