I have joined the Oxford University Computing Lab on April 1st 2009. Please update your bookmarks and proceed to my new webpage.

Philipp Rümmer (PhD Student, Chalmers University)

Since September 2004 I am doing my PhD in Computer Science at the Chalmers University, Gothenburg. My supervisor is Wolfgang Ahrendt. I am member of the formal methods group, and I am particularly interested in verification of imperative and/or concurrent programs, theorem proving, and in disproving. I am also member of the KeY project.

One of my current projects is the Princess theorem prover.

Update: I defended my PhD thesis on December 17th, 2008.

Philipp Rümmer
Department of Computer Science and Engineering
Chalmers University of Technology and Göteborg University
412-96 Göteborg, Sweden
Room: 5451A, Computer Science and Engineering Building
Mail: ph_r@gmx.net, philipp@chalmers.se
Tel: +46 (0)31 772 1072
GPG/PGP5-Key

Recent Publications and Workshop Papers

Philipp Rümmer
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Doha, Qatar, 2008
Springer-Verlag, LNCS 5330, pages 274-289
(Preliminary PDF - BibTeX - Abstract - Implementation)
My PhD thesis contains an extended version of the paper.
Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
Integration of a Security Type System into a Program Logic
Theoretical Computer Science, Volume 402, Issues 2-3, 8 August 2008, pages 172-189
(Special Issue with selected papers from TGC 2006)
(Preliminary PDF - BibTeX - Abstract)
Helga Velroyen, Philipp Rümmer
Non-Termination Checking for Imperative Programs
2nd International Conference on Tests and Proofs, Prato, Italy, 2008
Springer-Verlag, LNCS 4966, pages 154-170
(Preliminary PDF - BibTeX - Abstract - Implementation)
Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer
Integrating Verification and Testing of Object-Oriented Software
2nd International Conference on Tests and Proofs, Prato, Italy, 2008
Springer-Verlag, LNCS 4966, pages 182-191
(Tutorial paper)
(Preliminary PDF - BibTeX - Abstract)
Philipp Rümmer
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
4th International Verification Workshop at CADE 21, Bremen, Germany, July 2007
CEUR Workshop Proceedings, Vol 259
(PDF - BibTeX - Abstract)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt
Verifying Object-Oriented Programs with KeY: A Tutorial
5th International Symposium on Formal Methods for Components and Objects, Amsterdam, The Netherlands, November 2006
Springer-Verlag, LNCS 4709, pages 70-101
(Preliminary PDF - BibTeX - Abstract - Example of the paper - Talk)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
The KeY System (Deduction Component)
System abstract, International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007
Springer-Verlag, LNCS 4603, pages 379-384
(Preliminary PDF - BibTeX - Abstract)
Philipp Rümmer, Muhammad Ali Shah
Proving Programs Incorrect using a Sequent Calculus for Java Dynamic Logic
International Conference on Tests And Proofs (TAP), ETH Zürich, Switzerland
Springer-Verlag, LNCS 4454, pages 41-60
(Preliminary PDF - BibTeX - Abstract)
Philipp Rümmer
Construction of Proofs
Chapter in: Verification of Object-Oriented Software: The KeY Approach
Springer-Verlag, LNCS 4334, pages 177-242
(SpringerLink - BibTeX)
Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
Integration of a Security Type System into a Program Logic
2nd Symposium on Trustworthy Global Computing (TGC), Lucca, Italy
Springer-Verlag, LNCS 4661, pages 116-131
(Preliminary PDF - BibTeX - Abstract)
Philipp Rümmer
Sequential, Parallel, and Quantified Updates of First-Order Structures
13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Phnom Penh, Cambodia
Springer-Verlag, LNCS 4246, pages 422-436
(PDF (preprint) - BibTeX - Abstract)
An extended version of the paper is part of my licentiate thesis (below)
There is also a formalisation of theorems given in the paper in Isabelle/HOL
Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
Verification of JCSP Programs
Communicating Process Architectures 2005, volume 63 of Concurrent Systems Engineering Series, pages 203-218, IOS Press, The Netherlands, September 2005. IOS Press
(PDF - BibTeX - Abstract)
Philipp Rümmer
Generating Counterexamples for Java Dynamic Logic
Preliminary Proceedings of Workshop on Disproving at CADE 20, 2005
(Postscript - BibTeX - Abstract)

Theses, Technical Reports

Philipp Rümmer
Calculi for Program Incorrectness and Arithmetic
PhD Thesis, December 2008
Department of Computer Science and Engineering, University of Gothenburg
Technical Report no. D50
(PDF, Abstract - BibTeX)
Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
Integration of a Security Type System into a Program Logic
Technical Report no. 2007:1
(PDF - BibTeX - Abstract)
Philipp Rümmer
Proving and Disproving in Dynamic Logic for Java
Licentiate Thesis, August 2006
Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University
Technical Report no. 2006-26L
(PDF - BibTeX - Abstract)
Philipp Rümmer
Interactive Verification of JCSP Programs
Technical Report no. 2005-01
Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University
(Postscript - BibTeX - Abstract)

Teaching

Objektorienterad systemutveckling IT, HT 2004 - VT 2005
Software Engineering using Formal Methods, 2005
Objektorienterad systemutveckling IT, HT 2005 - VT 2006
Software Engineering using Formal Methods, 2006
Objektorienterad systemutveckling IT, HT 2006 - VT 2007
Software Engineering using Formal Methods, 2007

While I was studying in Karlsruhe ...

While I was studying at the University of Karlsruhe (between 1999 and 2004), I have worked for the KeY-Project as a student assistant (I am also member of the project nowadays). The project is about specification and deductive verification of JavaCard programs. Publications I have (co)authored when I was in Karlsruhe are:

Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager
Taclets – A new paradigm for constructing interactive theorem provers
Revista de la Real Academia de Ciencias, Físicas Y Naturales, Serie A: Matemáticas, 98 (1), 2004.
(PDF - BibTeX - Abstract)
Richard Bubel, Andreas Roth, and Philipp Rümmer
Ensuring Correctness of Lightweight Tactics for Java Card Dynamic Logic
Workshop on Logical Frameworks and Meta-Languages (LFM) at IJCAR 2004, 2004
ENTCS Volume 199, 24 February 2008, Pages 107-128
(Preliminary PDF - DOI - BibTeX - Abstract)
Philipp Rümmer
Ensuring the Soundness of Taclets - Constructing Proof Obligations for Java Card DL Taclets
Minor Thesis, University of Karlsruhe, 2003
(PDF - BibTeX)

Last update: by Philipp Rümmer

Disclaimer