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
- Chen, Taolue, Hague, Matthew, He, Jinlong, Hu, Denghang, Lin, Anthony Widjaja, Rümmer, Philipp and Wu, Zhilin (2020) A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type.
: 12302, P. 325—342.
https://dx.doi.org/10.1007/978-3-030-59152-6_18 - Chen, Taolue, Hague, Matthew, He, Jinlong, Hu, Denghang, Lin, Anthony Widjaja, Rümmer, Philipp and Wu, Zhilin (2020) A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type.
CoRR: abs/2007.06913 - Esen, Zafer and Rümmer, Philipp (2020) Abstract: Towards an SMT-LIB Theory of Heap.
: 2854, P. 60. - Rümmer, Philipp (2020) Competition Report: CHC-COMP-20.
: 320, P. 197—219.
https://dx.doi.org/10.4204/EPTCS.320.15 - Alshnakat, Anoud, Gurov, Dilian, Lidström, Christian and Rümmer, Philipp (2020) Constraint-Based Contract Inference for Deductive Verification.
: 12345, P. 149—176.
https://dx.doi.org/10.1007/978-3-030-64354-6_6 - Rümmer, Philipp (2020) Invited Talk: Solving String Constraints, Starting from the Beginning and from the End.
: 2854, P. 1. - (2020) Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual).
: 2752 - Hague, Matthew, Lin, Anthony W., Rümmer, Philipp and Wu, Zhilin (2020) Monadic Decomposition in Integer Linear Arithmetic.
: 12166, P. 122—140.
https://dx.doi.org/10.1007/978-3-030-51074-9_8 - Hague, Matthew, Lin, Anthony Widjaja, Rümmer, Philipp and Wu, Zhilin (2020) Monadic Decomposition in Integer Linear Arithmetic (Technical Report).
CoRR: abs/2004.12371 - Hong, Chih-Duo, Lin, Anthony W., Majumdar, Rupak and Rümmer, Philipp (2020) Probabilistic Bisimulation for Parameterized Systems (Technical Report).
CoRR: abs/2011.02413 - Esen, Zafer and Rümmer, Philipp (2020) Reasoning in the Theory of Heap: Satisfiability and Interpolation.
: 12561, P. 173—191.
https://dx.doi.org/10.1007/978-3-030-68446-4_9 - Lin, Anthony W. and Rümmer, Philipp (2020) Regular Model Checking Revisited (Technical Report).
CoRR: abs/2005.00990 - Hol\'ık, Lukás, Janku, Petr, Lin, Anthony W., Rümmer, Philipp and Vojnar, Tomás (2020) String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report).
CoRR: abs/2010.15975 - Chen, Taolue, Hague, Matthew, Lin, Anthony W., Rümmer, Philipp and Wu, Zhilin (2019) Decision procedures for path feasibility of string-manipulating programs with complex operations.
Proc. ACM Program. Lang.: 3 (POPL), P. 49:1—49:30.
https://dx.doi.org/10.1145/3290362 - Fuhs, Carsten, Rümmer, Philipp, Schmidt, Renate A. and Tinelli, Cesare (2019) Deduction Beyond Satisfiability (Dagstuhl Seminar 19371).
Dagstuhl Reports: 9 (9), P. 23—44.
https://dx.doi.org/10.4230/DAGREP.9.9.23 - Rümmer, Philipp (2019) JayHorn: a Java model checker.
, P. 1:1.
https://dx.doi.org/10.1145/3340672.3341113 - Kahsai, Temesghen, Rümmer, Philipp and Schäf, Martin (2019) JayHorn: A Java Model Checker - (Competition Contribution).
: 11429, P. 214—218.
https://dx.doi.org/10.1007/978-3-030-17502-3_16 - Hojjat, Hossein, Rümmer, Philipp and Shamakhi, Ali (2019) On Strings in Software Model Checking.
: 11893, P. 19—30.
https://dx.doi.org/10.1007/978-3-030-34175-6_2 - Hong, Chih-Duo, Lin, Anthony W., Majumdar, Rupak and Rümmer, Philipp (2019) Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols).
: 11561, P. 455—474.
https://dx.doi.org/10.1007/978-3-030-25540-4_27 - Klebanov, Vladimir, Rümmer, Philipp and Ulbrich, Mattias (2018) Automating regression verification of pointer programs by predicate abstraction.
Formal Methods Syst. Des.: 52 (3), P. 229—259.
https://dx.doi.org/10.1007/S10703-017-0293-8 - Backeman, Peter, Rümmer, Philipp and Zeljic, Aleksandar (2018) Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction.
, P. 1—10.
https://dx.doi.org/10.23919/FMCAD.2018.8603023 - Hojjat, Hossein and Rümmer, Philipp (2018) Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report).
CoRR: abs/1801.02367 - Chen, Taolue, Hague, Matthew, Lin, Anthony W., Rümmer, Philipp and Wu, Zhilin (2018) Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations.
CoRR: abs/1811.03167 - Zeljic, Aleksandar, Backeman, Peter, Wintersteiger, Christoph M. and Rümmer, Philipp (2018) Exploring Approximations for Floating-Point Arithmetic Using UppSAT.
: 10900, P. 246—262.
https://dx.doi.org/10.1007/978-3-319-94205-6_17 - (2018) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018.
: 2162