Prof. Dr. Philipp Rümmer
Lehrstuhlinhaber
- E-Mail Adresse: philipp.ruemmer(at)ur.de (?ffnet Ihr E-Mail-Programm)
- Tel: +49 941 943 - 68612 (startet einen Telefonanruf, wenn Ihr Ger?t dies zul?sst)
- Standort: Bajuwarenstr. 4, BA 602
- Lehrstuhl für Theoretische Informatik

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