Philipp Rümmer
Senior Lecturer/Associate Professor at Department of Information Technology; Division of Computer Systems
- Mobile phone:
- +46 76 853 17 87
- E-mail:
- Philipp.Ruemmer@it.uu.se
- Visiting address:
- Hus 10, Regementsvägen 10
- Postal address:
- Box 337
751 05 UPPSALA
Short presentation
Associate professor at the Division of Computer Systems, with main research focus on analysis of software and embedded systems. For more information, please visit my personal web page.

Publications
Recent publications
Complementable Normal Form of Parametrized Automata
Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 1-14, 2026
A New Approach for Showing Termination of Parameterized Transition Systems
Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 193-207, 2026
2025
OSTRICH2: Solver for Complex String Constraints
Part of Formal Methods in Computer Aided Design, FMCAD 2025, Menlo Park, California, USA, 2025
Part of Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, p. 56-80, 2025
All publications
Articles in journal
The Power of Regular Constraint Propagation
Part of Proceedings of the ACM on Programming Languages, p. 3203-3231, 2025
- DOI for The Power of Regular Constraint Propagation
- Download full text (pdf) of The Power of Regular Constraint Propagation
Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
Part of IEEE Transactions on Software Engineering, p. 1801-1817, 2025
A Constraint Solving Approach to Parikh Images of Regular Languages
Part of Proceedings of the ACM on Programming Languages, 2024
- DOI for A Constraint Solving Approach to Parikh Images of Regular Languages
- Download full text (pdf) of A Constraint Solving Approach to Parikh Images of Regular Languages
Scheduling Dynamic Software Updates in Mobile Robots
Part of ACM Transactions on Embedded Computing Systems, p. 1-27, 2023
- DOI for Scheduling Dynamic Software Updates in Mobile Robots
- Download full text (pdf) of Scheduling Dynamic Software Updates in Mobile Robots
Part of Proceedings of the ACM on Programming Languages, 2022
- DOI for Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
- Download full text (pdf) of Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Part of Formal methods in system design, p. 121-156, 2021
- DOI for Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Download full text (pdf) of Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Decision procedures for path feasibility of string-manipulating programs with complex operations
Part of Proceedings of the ACM on Programming Languages, 2019
- DOI for Decision procedures for path feasibility of string-manipulating programs with complex operations
- Download full text (pdf) of Decision procedures for path feasibility of string-manipulating programs with complex operations
String constraints with concatenation and transducers solved efficiently
Part of Proceedings of the ACM on Programming Languages, p. 1-32, 2018
- DOI for String constraints with concatenation and transducers solved efficiently
- Download full text (pdf) of String constraints with concatenation and transducers solved efficiently
Automating regression verification of pointer programs by predicate abstraction
Part of Formal methods in system design, p. 229-259, 2018
- DOI for Automating regression verification of pointer programs by predicate abstraction
- Download full text (pdf) of Automating regression verification of pointer programs by predicate abstraction
Flatten and Conquer: A Framework for Efficient Analysis of String Constraints
Part of SIGPLAN notices, p. 602-617, 2017
Preface to special issue on satisfiability modulo theories
Part of Formal methods in system design, p. 431-432, 2017
An approximation framework for solvers and decision procedures
Part of Journal of automated reasoning, p. 127-147, 2017
Preface, Electronic Proceedings in Theoretical Computer Science. Vol 219
Part of Electronic Proceedings in Theoretical Computer Science, 2016
Guiding Craig interpolation with domain-specific abstractions
Part of Acta Informatica, p. 387-424, 2016
- DOI for Guiding Craig interpolation with domain-specific abstractions
- Download full text (pdf) of Guiding Craig interpolation with domain-specific abstractions
On recursion-free Horn clauses and Craig interpolation
Part of Formal methods in system design, p. 1-25, 2015
Ranking function synthesis for bit-vector relations
Part of Formal methods in system design, p. 93-120, 2013
Automatic analysis of DMA races using model checking and k-induction
Part of Formal methods in system design, p. 83-113, 2011
An interpolating sequent calculus for quantifier-free Presburger arithmetic
Part of Journal of automated reasoning, p. 341-367, 2011
Chapters in book
Part of The Combined Power of Research, Education, and Dissemination, p. 259-279, Springer, 2025
Regular Model Checking Revisited
Part of Model Checking, Synthesis, and Learning, p. 97-114, Springer, 2022
Constraint-based Contract Inference for Deductive Verification
Part of Deductive Software Verification: Future Perspectives, p. 149-176, Springer Nature, 2020
Characterization of simulation by probabilistic testing
Part of Theory and Practice of Formal Methods, p. 360-372, Springer, 2016
Conference papers
Complementable Normal Form of Parametrized Automata
Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 1-14, 2026
A New Approach for Showing Termination of Parameterized Transition Systems
Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 193-207, 2026
OSTRICH2: Solver for Complex String Constraints
Part of Formal Methods in Computer Aided Design, FMCAD 2025, Menlo Park, California, USA, 2025
Part of Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, p. 56-80, 2025
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses
Part of Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, p. 200-214, 2025
What's Decidable About Arrays With Sums?
Part of Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, p. 56-74, 2025
Decision Procedure for a Theory of String Sequences
Part of Programming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, p. 217-238, 2025
2025
Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software
Part of Coordination Models and Languages, p. 90-113, 2025
Finding Universally Quantified Heap Invariants by Horn Clause Transformations
Part of Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, p. 42-60, 2025
Guiding Word Equation Solving using Graph Neural Networks
Part of Automated Technology for Verification and Analysi, p. 279-301, 2024
Boosting Constrained Horn Solving by Unsat Core Learning
Part of Verification, Model Checking, and Abstract Interpretation, p. 280-302, 2024
Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments
Part of HOTMOBILE '24, p. 138-138, 2024
- DOI for Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments
- Download full text (pdf) of Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments
An Encoding for CLP Problems in SMT-LIB
Part of Electronic Proceedings in Theoretical Computer Science, p. 118-130, 2024
- DOI for An Encoding for CLP Problems in SMT-LIB
- Download full text (pdf) of An Encoding for CLP Problems in SMT-LIB
Timing Analysis of Embedded Software Updates
2023
Automatic Program Instrumentation for Automatic Verification
Part of CAV 2023, p. 281-304, 2023
Decision Procedures for Sequence Theories
Part of CAV 2023: Computer Aided Verification, p. 18-40, 2023
An Active Learning Approach to Synthesizing Program Contracts
Part of Software Engineering and Formal Methods, SEFM 2023, p. 126-144, 2023
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
Part of AUTOMATED DEDUCTION, CADE 29, p. 170-189, 2023
- DOI for A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- Download full text (pdf) of A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
An Active Learning Approach to Synthesizing Program Contracts
2023
Part of Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), p. 38-53, 2022
TriCo—Triple Co-piloting of Implementation, Specification and Tests
Part of ISoLA 2022: Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, p. 174-187, 2022
TRICERA: Verifying C Programs Using the Theory of Heaps
Part of Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, p. 380-391, 2022
- DOI for TRICERA: Verifying C Programs Using the Theory of Heaps
- Download full text (pdf) of TRICERA: Verifying C Programs Using the Theory of Heaps
Exploring Representation of Horn clauses using GNNs
Part of PAAR’22, 2022
OptiRica: Towards an Efficient Optimizing Horn Solver
Part of Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, p. 35-43, 2022
- DOI for OptiRica: Towards an Efficient Optimizing Horn Solver
- Download full text (pdf) of OptiRica: Towards an Efficient Optimizing Horn Solver
Part of 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), p. 284-285, 2022
- DOI for Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems: the Case of Aerial Drones
- Download full text (pdf) of Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems: the Case of Aerial Drones
CertiStr: A Certified String Solver
Part of CPP 2022, p. 210-224, 2022
- DOI for CertiStr: A Certified String Solver
- Download full text (pdf) of CertiStr: A Certified String Solver
NeRTA: Enabling Dynamic Software Updates in Mobile Robotics
2022
Towards String Support in JayHorn (Competition Contribution)
Part of Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021, p. 443-447, 2021
Reasoning in the Theory of Heap: Satisfiability and Interpolation
Part of LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2020, p. 173-191, 2021
Competition Report: CHC-COMP-21
Part of Electronic Proceedings in Theoretical Computer Science, p. 91-108, 2021
Monadic Decomposition in Integer Linear Arithmetic
Part of IJCAR 2020, p. 122-140, 2020
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Part of ATVA 2020, p. 325-342, 2020
Competition Report: CHC-COMP-20
Part of Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, p. 197-219, 2020
JayHorn: A Java Model Checker -: (Competition Contribution)
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 214-218, 2019
- DOI for JayHorn: A Java Model Checker -: (Competition Contribution)
- Download full text (pdf) of JayHorn: A Java Model Checker -: (Competition Contribution)
On Strings in Software Model Checking
Part of Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, p. 19-30, 2019
Part of PROCEEDINGS OF THE 21ST WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2019), 2019
Part of Computer Aided Verification. CAV 2019., p. 455-474, 2019
- DOI for Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols)
- Download full text (pdf) of Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols)
Trau: SMT solver for string constraints
Part of Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018
Exploring Approximations for Floating-Point Arithmetic using UppSAT
Part of Automated Reasoning, p. 246-262, 2018
- DOI for Exploring Approximations for Floating-Point Arithmetic using UppSAT
- Download full text (pdf) of Exploring Approximations for Floating-Point Arithmetic using UppSAT
Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
Part of Formal Methods in Computer-Aided Design, p. 50-59, 2018
- DOI for Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
- Download full text (pdf) of Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
Part of Formal Methods in Computer Aided Design, p. 158-164, 2018
Systematic predicate abstraction using variable roles
Part of NASA Formal Methods, p. 265-281, 2017
- DOI for Systematic predicate abstraction using variable roles
- Download full text (pdf) of Systematic predicate abstraction using variable roles
Deciding and Interpolating Algebraic Data Types by Reduction
Part of 2017 19th international symposium on symbolic and numeric algorithms for scientific computing (SYNASC 2017), p. 145-152, 2017
Fair termination for parameterized probabilistic concurrent systems
Part of Tools and Algorithms for the Construction and Analysis of Systems, p. 499-517, 2017
- DOI for Fair termination for parameterized probabilistic concurrent systems
- Download full text (pdf) of Fair termination for parameterized probabilistic concurrent systems
Learning to prove safety over parameterised concurrent systems
Part of Proceedings of the 17th International Conference on Formal Methods in Computer-Aided Design, p. 76-83, 2017
- DOI for Learning to prove safety over parameterised concurrent systems
- Download full text (pdf) of Learning to prove safety over parameterised concurrent systems
Quantified heap invariants for object-oriented programs
Part of 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, p. 368-384, 2017
Optimizing Horn Solvers for Network Repair
Part of Proceedings of the 2016 16Th Conference on Formal Methods In Computer-Aided Design (FMCAD 2016), p. 73-80, 2016
Deciding bit-vector formulas with mcSAT
Part of Theory and Applications of Satisfiability Testing, p. 249-266, 2016
Liveness of randomised parameterised systems under arbitrary schedulers
Part of Computer Aided Verification, p. 112-133, 2016
- DOI for Liveness of randomised parameterised systems under arbitrary schedulers
- Download full text (pdf) of Liveness of randomised parameterised systems under arbitrary schedulers
JayHorn: A framework for verifying Java programs
Part of Computer Aided Verification, p. 352-358, 2016
- DOI for JayHorn: A framework for verifying Java programs
- Download full text (pdf) of JayHorn: A framework for verifying Java programs
A Comparative Study of GPUVerify and GKLEE
Part of 2016 Fourth International Conference On Parallel, Distributed And Grid Computing (PDGC), p. 112-117, 2016
Part of Verification, Model Checking, and Abstract Interpretation, p. 455-475, 2016
Norn: An SMT solver for string constraints
Part of Computer Aided Verification, p. 462-469, 2015
Bixie: Finding and understanding inconsistent code
Part of Proc. 37th IEEE/ACM International Conference on Software Engineering, p. 645-648, 2015
Free variables and theories: Revisiting rigid E-unification
Part of Frontiers of Combining Systems, p. 3-13, 2015
- DOI for Free variables and theories: Revisiting rigid E-unification
- Download full text (pdf) of Free variables and theories: Revisiting rigid E-unification
An automatable formal semantics for IEEE-754 floating-point arithmetic
Part of Proc. 22nd Symposium on Computer Arithmetic, p. 160-167, 2015
Theorem proving with bounded rigid E-unification
Part of Automated Deduction – CADE-25, p. 572-587, 2015
Automating regression verification
Part of Software Engineering & Management 2015, p. 75-76, 2015
Conflict-Directed Graph Coverage
Part of NASA FORMAL METHODS (NFM 2015), p. 327-342, 2015
Efficient algorithms for bounded rigid E-unification
Part of Automated Reasoning with Analytic Tableaux and Related Methods, p. 70-85, 2015
- DOI for Efficient algorithms for bounded rigid E-unification
- Download full text (pdf) of Efficient algorithms for bounded rigid E-unification
Automating regression verification
Part of ASE '14 Proceedings of the 29th ACM/IEEE international conference on Automated software engineering, p. 349-360, 2014
Horn Clauses for Communicating Timed Systems
Part of Proceedings First Workshop on Horn Clauses for Verification and Synthesis, p. 39-52, 2014
- DOI for Horn Clauses for Communicating Timed Systems
- Download full text (pdf) of Horn Clauses for Communicating Timed Systems
Part of NASA Formal Methods, p. 313-327, 2014
Approximations for Model Construction
Part of Automated Reasoning, p. 344-359, 2014
- DOI for Approximations for Model Construction
- Download full text (pdf) of Approximations for Model Construction
String Constraints for Verification
Part of Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, p. 150-166, 2014
A theory for control-flow graph exploration
Part of Automated Technology for Verification and Analysis, p. 506-515, 2013
Part of Formal Methods in Computer-Aided Design (FMCAD), 2013
Disjunctive Interpolants for Horn-Clause Verification
Part of Computer Aided Verification, p. 347-363, 2013
Classifying and Solving Horn Clauses for Verification
Part of Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), 2013
A verification toolkit for numerical transition systems
Part of FM 2012, p. 247-251, 2012
E-matching with free variables
Part of Logic for Programming, Artificial Intelligence, and Reasoning, p. 359-374, 2012
Part of Automated Technology for Verification and Analysis, p. 187-202, 2012
Tightening test coverage metrics: A case study in equivalence checking using k-induction
Part of Formal Methods for Components and Objects, p. 297-315, 2011
Test-case generation for embedded Simulink via formal concept analysis
Part of Proc. 48th Design Automation Conference, p. 224-229, 2011
SCRATCH: a tool for automatic analysis of DMA races
Part of Proc. 16th ACM Symposium on Principles and Practice of Parallel Programming, p. 311-312, 2011
Software verification using k-induction
Part of Static Analysis, p. 351-368, 2011
Beyond quantifier-free interpolation in extensions of Presburger arithmetic
Part of Verification, Model Checking, and Abstract Interpretation, p. 88-102, 2011