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
- Lin, Anthony W., Nguyen, Truong Khanh, Rümmer, Philipp and Sun, Jun (2016) Regular Symmetry Patterns.
: 9583, P. 455—475.
https://dx.doi.org/10.1007/978-3-662-49122-5_22 - Brain, Martin, Tinelli, Cesare, Rümmer, Philipp and Wahl, Thomas (2015) An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.
, P. 160—167.
https://dx.doi.org/10.1109/ARITH.2015.26 - Felsing, Dennis, Grebing, Sarah, Klebanov, Vladimir, Rümmer, Philipp and Ulbrich, Mattias (2015) Automating Regression Verification.
: P-239, P. 75—76. - McCarthy, Tim, Rümmer, Philipp and Sch?f, Martin (2015) Bixie: Finding and Understanding Inconsistent Code.
, P. 645—648.
https://dx.doi.org/10.1109/ICSE.2015.213 - Schwartz-Narbonne, Daniel, Sch?f, Martin, Jovanovic, Dejan, Rümmer, Philipp and Wies, Thomas (2015) Conflict-Directed Graph Coverage.
: 9058, P. 327—342.
https://dx.doi.org/10.1007/978-3-319-17524-9_23 - Backeman, Peter and Rümmer, Philipp (2015) Efficient Algorithms for Bounded Rigid E-unification.
: 9323, P. 70—85.
https://dx.doi.org/10.1007/978-3-319-24312-2_6 - Backeman, Peter and Rümmer, Philipp (2015) Free Variables and Theories: Revisiting Rigid E-unification.
: 9322, P. 3—13.
https://dx.doi.org/10.1007/978-3-319-24246-0_1 - Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Chen, Yu-Fang, Hol\'?k, Lukás, Rezine, Ahmed, Rümmer, Philipp and Stenman, Jari (2015) Norn: An SMT Solver for String Constraints.
: 9206, P. 462—469.
https://dx.doi.org/10.1007/978-3-319-21690-4_29 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2015) On recursion-free Horn clauses and Craig interpolation.
Formal Methods Syst. Des.: 47 (1), P. 1—25.
https://dx.doi.org/10.1007/S10703-014-0219-7 - Lin, Anthony W., Nguyen, Truong Khanh, Rümmer, Philipp and Sun, Jun (2015) Regular Symmetry Patterns (Technical Report).
CoRR: abs/1510.08506 - Backeman, Peter and Rümmer, Philipp (2015) Theorem Proving with Bounded Rigid E-Unification.
: 9195, P. 572—587.
https://dx.doi.org/10.1007/978-3-319-21401-6_39 - Zeljic, Aleksandar, Wintersteiger, Christoph M. and Rümmer, Philipp (2014) Approximations for Model Construction.
: 8562, P. 344—359.
https://dx.doi.org/10.1007/978-3-319-08587-6_26 - Felsing, Dennis, Grebing, Sarah, Klebanov, Vladimir, Rümmer, Philipp and Ulbrich, Mattias (2014) Automating regression verification.
, P. 349—360.
https://dx.doi.org/10.1145/2642937.2642987 - Hojjat, Hossein, Rümmer, Philipp, Subotic, Pavle and Yi, Wang (2014) Horn Clauses for Communicating Timed Systems.
: 169, P. 39—52.
https://dx.doi.org/10.4204/EPTCS.169.6 - (2014) Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, affiliated with the 26th International Conference on Computer Aided Verification (CAV 2014), the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, July 17-18, 2014.
: 1163 - Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Chen, Yu-Fang, Hol\'?k, Lukás, Rezine, Ahmed, Rümmer, Philipp and Stenman, Jari (2014) String Constraints for Verification.
: 8559, P. 150—166.
https://dx.doi.org/10.1007/978-3-319-08867-9_10 - Arlt, Stephan, Rubio-González, Cindy, Rümmer, Philipp, Sch?f, Martin and Shankar, Natarajan (2014) The Gradual Verifier.
: 8430, P. 313—327.
https://dx.doi.org/10.1007/978-3-319-06200-6_27 - Arlt, Stephan, Rümmer, Philipp and Sch?f, Martin (2013) A Theory for Control-Flow Graph Exploration.
: 8172, P. 506—515.
https://dx.doi.org/10.1007/978-3-319-02444-8_44 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Classifying and Solving Horn Clauses for Verification.
: 8164, P. 1—21.
https://dx.doi.org/10.1007/978-3-642-54108-7_1 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Disjunctive Interpolants for Horn-Clause Verification.
: 8044, P. 347—363.
https://dx.doi.org/10.1007/978-3-642-39799-8_24 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report).
CoRR: abs/1301.4973 - Rümmer, Philipp and Subotic, Pavle (2013) Exploring interpolants.
, P. 69—76. - Arlt, Stephan, Rümmer, Philipp and Sch?f, Martin (2013) Joogie: from Java through Jimple to Boogie.
, P. 3—8.
https://dx.doi.org/10.1145/2487568.2487570 - Cook, Byron, Kroening, Daniel, Rümmer, Philipp and Wintersteiger, Christoph M. (2013) Ranking function synthesis for bit-vector relations.
Formal Methods Syst. Des.: 43 (1), P. 93—120.
https://dx.doi.org/10.1007/S10703-013-0186-4 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) The Relationship between Craig Interpolation and Recursion-Free Horn Clauses.
CoRR: abs/1302.4187