Prof. Dr. Philipp Rümmer
Head of Chair
- E-mail address: philipp.ruemmer(at)ur.de (opens your email program)
- Tel: +49 941 943 - 68612 (starts a telephone call, if your device allows this)
- Location: Bajuwarenstr. 4, BA 602
- Theoretical Computer Science Group

More information about Philipp Rümmer can be found on his personal website (external link, opens in a new window).
Publications
- Hojjat, Hossein, Konecn?, Filip, Garnier, Florent, Iosif, Radu, Kuncak, Viktor and Rümmer, Philipp (2012) A Verification Toolkit for Numerical Transition Systems - Tool Paper.
: 7436, P. 247—251.
https://dx.doi.org/10.1007/978-3-642-32759-9_21 - Hojjat, Hossein, Iosif, Radu, Konecn?, Filip, Kuncak, Viktor and Rümmer, Philipp (2012) Accelerating Interpolants.
: 7561, P. 187—202.
https://dx.doi.org/10.1007/978-3-642-33386-6_16 - Rümmer, Philipp (2012) Craig Interpolation for the Integers: Results, Implementation, and Experiences.
: 22, P. 3.
https://dx.doi.org/10.29007/9RXZ - Rümmer, Philipp (2012) E-Matching with Free Variables.
: 7180, P. 359—374.
https://dx.doi.org/10.1007/978-3-642-28717-6_28 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2011) An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
J. Autom. Reason.: 47 (4), P. 341—367.
https://dx.doi.org/10.1007/S10817-011-9237-Y - Donaldson, Alastair F., Kroening, Daniel and Rümmer, Philipp (2011) Automatic analysis of DMA races using model checking and \emphk-induction.
Formal Methods Syst. Des.: 39 (1), P. 83—113.
https://dx.doi.org/10.1007/S10703-011-0124-2 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2011) Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.
: 6538, P. 88—102.
https://dx.doi.org/10.1007/978-3-642-18275-4_8 - Donaldson, Alastair F., Kroening, Daniel and Rümmer, Philipp (2011) SCRATCH: a tool for automatic analysis of dma races.
, P. 311—312.
https://dx.doi.org/10.1145/1941553.1941604 - Donaldson, Alastair F., Haller, Leopold, Kroening, Daniel and Rümmer, Philipp (2011) Software Verification Using k-Induction.
: 6887, P. 351—368.
https://dx.doi.org/10.1007/978-3-642-23702-7_26 - He, Nannan, Rümmer, Philipp and Kroening, Daniel (2011) Test-case generation for embedded simulink via formal concept analysis.
, P. 224—229.
https://dx.doi.org/10.1145/2024724.2024777 - Leino, K. Rustan M. and Rümmer, Philipp (2010) A Polymorphic Intermediate Verification Language: Design and Logical Encoding.
: 6015, P. 312—327.
https://dx.doi.org/10.1007/978-3-642-12002-2_26 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2010) An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
: 6173, P. 384—399.
https://dx.doi.org/10.1007/978-3-642-14203-1_33 - Donaldson, Alastair F., Kroening, Daniel and Rümmer, Philipp (2010) Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.
: 6015, P. 280—295.
https://dx.doi.org/10.1007/978-3-642-12002-2_24 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2010) Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report).
CoRR: abs/1011.1036 - Kroening, Daniel, Leroux, Jér?me and Rümmer, Philipp (2010) Interpolating Quantifier-Free Presburger Arithmetic.
: 6397, P. 489—503.
https://dx.doi.org/10.1007/978-3-642-16242-8_35 - Ahrendt, Wolfgang, Beckert, Bernhard, Giese, Martin and Rümmer, Philipp (2010) Practical Aspects of Automated Deduction for Program Verification.
Künstliche Intell.: 24 (1), P. 43—49.
https://dx.doi.org/10.1007/S13218-010-0001-Y - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2010) Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays.
: 3, P. 31—46.
https://dx.doi.org/10.29007/ZFKW - Cook, Byron, Kroening, Daniel, Rümmer, Philipp and Wintersteiger, Christoph M. (2010) Ranking Function Synthesis for Bit-Vector Relations.
: 6015, P. 236—250.
https://dx.doi.org/10.1007/978-3-642-12002-2_19 - Donaldson, Alastair F., He, Nannan, Kroening, Daniel and Rümmer, Philipp (2010) Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction.
: 6957, P. 297—315.
https://dx.doi.org/10.1007/978-3-642-25271-6_16 - Brillout, Angelo, He, Nannan, Mazzucchi, Michele, Kroening, Daniel, Purandare, Mitra, Rümmer, Philipp and Weissenbacher, Georg (2009) Mutation-Based Test Case Generation for Simulink Models.
: 6286, P. 208—227.
https://dx.doi.org/10.1007/978-3-642-17071-3_11 - Platzer, André, Quesel, Jan-David and Rümmer, Philipp (2009) Real World Verification.
: 5663, P. 485—501.
https://dx.doi.org/10.1007/978-3-642-02959-2_35 - Rümmer, Philipp (2008) A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.
: 5330, P. 274—289.
https://dx.doi.org/10.1007/978-3-540-89439-1_20 - Engel, Christian, Gladisch, Christoph, Klebanov, Vladimir and Rümmer, Philipp (2008) Integrating Verification and Testing of Object-Oriented Software.
: 4966, P. 182—191.
https://dx.doi.org/10.1007/978-3-540-79124-9_13 - H?hnle, Reiner, Pan, Jing, Rümmer, Philipp and Walter, Dennis (2008) Integration of a security type system into a program logic.
Theor. Comput. Sci.: 402 (2-3), P. 172—189.
https://dx.doi.org/10.1016/J.TCS.2008.04.033 - Velroyen, Helga and Rümmer, Philipp (2008) Non-termination Checking for Imperative Programs.
: 4966, P. 154—170.
https://dx.doi.org/10.1007/978-3-540-79124-9_11