Prof. Dr. Steffen Schlager
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