Skip to main content


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
To top