Peer-Reviewed Articles

2012

• Philipp Rümmer
  E-Matching with Free Variables
  18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mérida, Venezuela, March 2012
  To appear in LNCS
  (Preliminary PDF - BibTeX - Abstract)
• Alastair F. Donaldson, Nannan He, Philipp Rümmer, Daniel Kroening
  Tightening test coverage metrics: A case study in equivalence checking using k-induction
  9th International Symposium on Formal Methods for Components and Objects (FMCO), 2010, Graz, Austria. Revised Papers
  Springer-Verlag, LNCS 6957, pages 297-315
  (Preliminary PDF - BibTeX - Abstract)
  

2011

• Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
  An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
  Journal of Automated Reasoning, Volume 47 / 2011, Issue 4, Pages 341-367
  Special Issue on Selected Papers from the 5th International Joint Conference on Automated Reasoning (IJCAR)
  (Preliminary PDF - DOI - BibTeX - Abstract)
• Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
  Automatic Analysis of DMA Races Using Model Checking and k-induction
  International Journal on Formal Methods in System Design (FMSD), Volume 39 / 2011, Number 1, pages 83-113
  (Preliminary PDF - DOI - BibTeX - Abstract)
  
• Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer
  Software Verification Using k-Induction
  18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011
  Springer-Verlag, LNCS 6887, pages 351-368
  (Preliminary PDF - BibTeX - Abstract - Implementation)
  
• Nannan He, Philipp Rümmer, Daniel Kroening
  Test-case generation for embedded Simulink via formal concept analysis
  Design Automation Conference (DAC), San Diego, USA, June 2011
  Nominated for best-paper award
  (Preliminary PDF - BibTeX - Abstract)
  
• Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
  SCRATCH: a tool for automatic analysis of DMA races
  Poster at 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP), San Antonio, TX, USA, 2011
  (PDF - BibTeX - Abstract - Implementation)
  
• Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
  Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
  12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Austin, Texas, January 2011
  Springer-Verlag, LNCS 6538, pages 88-102
  (Preliminary PDF - BibTeX - Abstract - Implementation)
  

2010

• Daniel Kroening, Jérôme Leroux, Philipp Rümmer
  Interpolating Quantifier-Free Presburger Arithmetic
  17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Yogyakarta, Indonesia, October 2010
  Springer-Verlag, LNCS 6397, pages 489-503
  (Preliminary PDF - BibTeX - Abstract)
  
• Philipp Rümmer, Thomas Wahl
  An SMT-LIB Theory of Binary Floating-Point Arithmetic
  8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, Edinburgh, Scotland, July 2010
  (PDF - BibTeX - Abstract)
  
• Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
  Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
  6th International Verification Workshop (VERIFY) at FLoC, Edinburgh, Scotland, July 2010
  (PDF - BibTeX - Abstract - Implementation)
  
• Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
  An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
  International Joint Conference on Automated Reasoning (IJCAR) at FLoC, Edinburgh, Scotland, July 2010
  Springer-Verlag, LNCS 6173, pages 384-399
  (Preliminary PDF - BibTeX - Abstract)
• Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher
  Mutation-based Test Case Generation for Simulink Models
  International Symposium on Formal Methods for Components and Objects, Eindhoven, The Netherlands, November 2009
  Springer-Verlag, LNCS 6286, pages 208-227
  (Preliminary PDF - BibTeX - Abstract)
  
• Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
  Analysing DMA Races in Multicore Software
  3rd Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES'10) at ETAPS 2010
  (PDF - BibTeX - Abstract)
  
• Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
  Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
  16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
  Springer-Verlag, LNCS 6015, pages 280-295
  (Preliminary PDF - BibTeX - Abstract - Implementation)
  
• Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
  Ranking Function Synthesis for Bit-Vector Relations
  16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
  Springer-Verlag, LNCS 6015, pages 236-250
  (Preliminary PDF - BibTeX - Abstract - More information - Seneschal)
  
• K. Rustan M. Leino, Philipp Rümmer
  A Polymorphic Intermediate Verification Language: Design and Logical Encoding
  16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
  Springer-Verlag, LNCS 6015, pages 312-327
  (Preliminary PDF - BibTeX - Abstract)
  

2009

• Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer
  Practical Aspects of Automated Deduction for Program Verification
  KI Journal, Volume 24 / 2010, Number 1, pages 43-49
  (Preliminary PDF - BibTeX - Abstract)
  
• Daniel Kröning, Philipp Rümmer, Georg Weissenbacher
  A Proposal for a Theory of Finite Sets, Lists, and Maps for the SMT-Lib Standard
  7th International Workshop on Satisfiability Modulo Theories at CADE, Montreal, Canada, August 2009
  In informal workshop proceedings
  (PDF - BibTeX - Abstract)
  
• André Platzer, Jan-David Quesel, Philipp Rümmer
  Real World Verification
  22nd International Conference on Automated Deduction (CADE), Montreal, Canada, August 2009
  Springer-Verlag, LNCS 5663, pages 485-501
  (Preliminary PDF - BibTeX - Abstract - More information)
  

2008

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

2007

• 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)
• 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, Februrary 2007
  Springer-Verlag, LNCS 4454, pages 41-60
  (Preliminary PDF - BibTeX - Abstract)
  

2006

• 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)
  
• 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, November 2006
  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, November 2006
  Springer-Verlag, LNCS 4246, pages 422-436
  (PDF (preprint) - BibTeX - Abstract)
  My PhD thesis contains an extended version of the paper.
  There is also a formalisation of theorems given in the paper in Isabelle/HOL
  

2005

• Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
  Verification of JCSP Programs
  Communicating Process Architectures, Eindhoven, The Netherlands, September 2005
  IOS Press, volume 63 of Concurrent Systems Engineering Series, pages 203-218, The Netherlands
  (PDF - BibTeX - Abstract)
• Philipp Rümmer
  Generating Counterexamples for Java Dynamic Logic
  Informal Proceedings of Workshop on Disproving at CADE 20, 2005
  (Postscript - BibTeX - Abstract)