Philipp Rümmer

Sound and Complete Invariant-Based Heap Encodings

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Proceedings of the ACM on Programming Languages, p. 794-822, 2026

• DOI for Sound and Complete Invariant-Based Heap Encodings
• Download full text (pdf) of Sound and Complete Invariant-Based Heap Encodings

A program instrumentation framework for automatic verification

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidstrom, Christian et al.

Part of Formal methods in system design, 2026

• DOI for A program instrumentation framework for automatic verification
• Download full text (pdf) of A program instrumentation framework for automatic verification

Complementable Normal Form of Parametrized Automata

Alber, Franziska; Rümmer, Philipp

Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 1-14, 2026

• DOI for Complementable Normal Form of Parametrized Automata

A New Approach for Showing Termination of Parameterized Transition Systems

Herrmann, Roland; Rümmer, Philipp

Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 193-207, 2026

• DOI for A New Approach for Showing Termination of Parameterized Transition Systems

Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO

El Yaacoub, Ahmed; Voigt, Thiemo; Ruemmer, Philipp; Mottola, Luca

p. 48-59, 2025

• DOI for Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO
• Download full text (pdf) of Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO

Sound and Complete Invariant-Based Heap Encodings

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Proceedings of the ACM on Programming Languages, p. 794-822, 2026

• DOI for Sound and Complete Invariant-Based Heap Encodings
• Download full text (pdf) of Sound and Complete Invariant-Based Heap Encodings

A program instrumentation framework for automatic verification

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidstrom, Christian et al.

Part of Formal methods in system design, 2026

• DOI for A program instrumentation framework for automatic verification
• Download full text (pdf) of A program instrumentation framework for automatic verification

The Power of Regular Constraint Propagation

Hague, Matthew; Jez, Artur; Lin, Anthony Widjaja; Markgraf, Oliver et al.

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

Hong, Chih-Duo; Lin, Anthony W.; Rümmer, Philipp; Majumdar, Rupak

Part of IEEE Transactions on Software Engineering, p. 1801-1817, 2025

• DOI for Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

A Constraint Solving Approach to Parikh Images of Regular Languages

Stjerna, Amanda; Rümmer, Philipp

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

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp

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

Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables

Chen, Taolue; Flores-Lamas, Alejandro; Hague, Matthew; Han, Zhilei et al.

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

Backeman, Peter; Rümmer, Philipp; Zeljic, Aleksandar

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

Chen, Taolue; Hague, Matthew; Lin, Anthony W.; Rümmer, Philipp et al.

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

Holik, Lukas; Janku, Petr; Lin, Anthony W.; Rümmer, Philipp et al.

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

Klebanov, Vladimir; Rümmer, Philipp; Ulbrich, Mattias

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

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Bui, Phi Diep et al.

Part of SIGPLAN notices, p. 602-617, 2017

• DOI for Flatten and Conquer: A Framework for Efficient Analysis of String Constraints

Preface to special issue on satisfiability modulo theories

Griggio, Alberto; Rümmer, Philipp

Part of Formal methods in system design, p. 431-432, 2017

• DOI for Preface to special issue on satisfiability modulo theories

An approximation framework for solvers and decision procedures

Zeljic, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp

Part of Journal of automated reasoning, p. 127-147, 2017

• DOI for An approximation framework for solvers and decision procedures

Preface, Electronic Proceedings in Theoretical Computer Science. Vol 219

Gallagher, John; Rümmer, Philipp

Part of Electronic Proceedings in Theoretical Computer Science, 2016

Guiding Craig interpolation with domain-specific abstractions

Leroux, Jérôme; Rümmer, Philipp; Subotic, Pavle

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

Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor

Part of Formal methods in system design, p. 1-25, 2015

• DOI for On recursion-free Horn clauses and Craig interpolation

Ranking function synthesis for bit-vector relations

Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.

Part of Formal methods in system design, p. 93-120, 2013

• DOI for Ranking function synthesis for bit-vector relations

Automatic analysis of DMA races using model checking and k-induction

Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp

Part of Formal methods in system design, p. 83-113, 2011

• DOI for Automatic analysis of DMA races using model checking and k-induction

An interpolating sequent calculus for quantifier-free Presburger arithmetic

Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas

Part of Journal of automated reasoning, p. 341-367, 2011

• DOI for An interpolating sequent calculus for quantifier-free Presburger arithmetic

Timing is All You Need

Graf, Susanne; Jonsson, Bengt; Khodabandeloo, Behnam; Huang, Chengzi et al.

Part of The Combined Power of Research, Education, and Dissemination, p. 259-279, Springer, 2025

• DOI for Timing is All You Need

An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidström, Christian et al.

Part of Guide to Software Verification with Frama-C, p. 553-582, Springer Nature, 2024

• DOI for An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
• Download full text (pdf) of An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Regular Model Checking Revisited

Lin, Anthony W.; Rümmer, Philipp

Part of Model Checking, Synthesis, and Learning, p. 97-114, Springer, 2022

• DOI for Regular Model Checking Revisited

Constraint-based Contract Inference for Deductive Verification

Alshnakat, Anoud; Gurov, Dilian; Lidström, Christian; Rümmer, Philipp

Part of Deductive Software Verification: Future Perspectives, p. 149-176, Springer Nature, 2020

• DOI for Constraint-based Contract Inference for Deductive Verification

Characterization of simulation by probabilistic testing

Rümmer, Philipp; Yi, Wang

Part of Theory and Practice of Formal Methods, p. 360-372, Springer, 2016

• DOI for Characterization of simulation by probabilistic testing

Complementable Normal Form of Parametrized Automata

Alber, Franziska; Rümmer, Philipp

Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 1-14, 2026

• DOI for Complementable Normal Form of Parametrized Automata

A New Approach for Showing Termination of Parameterized Transition Systems

Herrmann, Roland; Rümmer, Philipp

Part of IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, p. 193-207, 2026

• DOI for A New Approach for Showing Termination of Parameterized Transition Systems

Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO

El Yaacoub, Ahmed; Voigt, Thiemo; Ruemmer, Philipp; Mottola, Luca

p. 48-59, 2025

• DOI for Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO
• Download full text (pdf) of Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO

Decision Procedure for a Theory of String Sequences

Hu, Denghang; Chen, Taolue; Rümmer, Philipp; Song, Fu et al.

Part of Programming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, p. 217-238, 2025

• DOI for Decision Procedure for a Theory of String Sequences

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses

Jiang, Hongjian; Lin, Anthony W.; Markgraf, Oliver; Rümmer, Philipp et al.

Part of Computer Aided Verification, p. 200-214, 2025

• DOI for HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses

OSTRICH2: Solver for Complex String Constraints

Hague, Matthew; Hu, Denghang; Jez, Artur; Lin, Anthony W. et al.

Part of Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025, p. 145, 2025

• DOI for OSTRICH2: Solver for Complex String Constraints
• Download full text (pdf) of OSTRICH2: Solver for Complex String Constraints

Arithmetizing Shape Analysis

Wolff, Sebastian; Gupta, Ekanshdeep; Esen, Zafer; Hojjat, Hossein et al.

Part of Computer Aided Verification, p. 56-80, 2025

• DOI for Arithmetizing Shape Analysis
• Download full text (pdf) of Arithmetizing Shape Analysis

What's Decidable About Arrays With Sums?

Herrmann, Roland; Rümmer, Philipp

Part of Proceeding of the Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction,, p. 56-74, 2025

• DOI for What's Decidable About Arrays With Sums?

When GNNs Met a Word Equations Solver: Learning to Rank Equations

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Frontiers of Combining Systems (FroCoS 2025), p. 327-345, 2025

• DOI for When GNNs Met a Word Equations Solver: Learning to Rank Equations

Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software

Huber, Nikolaus; Graf, Susanne; Rümmer, Philipp; Wang, Yi

Part of Coordination Models and Languages, p. 90-113, 2025

• DOI for Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software

Finding Universally Quantified Heap Invariants by Horn Clause Transformations

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

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

• DOI for Finding Universally Quantified Heap Invariants by Horn Clause Transformations

Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp

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

Guiding Word Equation Solving using Graph Neural Networks

Abdulla, Parosh; Atig, Mohamed Faouzi; Cailler, Julie; Liang, Chencheng et al.

Part of Automated Technology for Verification and Analysi, p. 279-301, 2024

• DOI for Guiding Word Equation Solving using Graph Neural Networks

Boosting Constrained Horn Solving by Unsat Core Learning

Abdulla, Parosh Aziz; Liang, Chencheng; Rümmer, Philipp

Part of Verification, Model Checking, and Abstract Interpretation, p. 280-302, 2024

• DOI for Boosting Constrained Horn Solving by Unsat Core Learning

An Encoding for CLP Problems in SMT-LIB

Amrollahi, Daneshvar; Hojjat, Hossein; Rümmer, Philipp

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

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp

2023

• DOI for Timing Analysis of Embedded Software Updates

Automatic Program Instrumentation for Automatic Verification

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidström, Christian et al.

Part of CAV 2023, p. 281-304, 2023

• DOI for Automatic Program Instrumentation for Automatic Verification

Decision Procedures for Sequence Theories

Jez, Artur; Lin, Anthony W.; Markgraf, Oliver; Rümmer, Philipp

Part of CAV 2023: Computer Aided Verification, p. 18-40, 2023

• DOI for Decision Procedures for Sequence Theories

An Active Learning Approach to Synthesizing Program Contracts

Ghosal, Sandip; Jonsson, Bengt; Rümmer, Philipp

Part of Software Engineering and Formal Methods, SEFM 2023, p. 126-144, 2023

• DOI for An Active Learning Approach to Synthesizing Program Contracts

A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)

Chen, Yu-Fang; Rümmer, Philipp; Tsai, Wei-Lun

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

Ghosal, Sandip; Jonsson, Bengt; Rümmer, Philipp

2023

An SMT-LIB Theory of Heaps

Esen, Zafer; Rümmer, Philipp

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

• Download full text (pdf) of An SMT-LIB Theory of Heaps

TriCo—Triple Co-piloting of Implementation, Specification and Tests

Ahrendt, Wolfgang; Gurov, Dilian; Johansson, Moa; Rümmer, Philipp

Part of ISoLA 2022: Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, p. 174-187, 2022

• DOI for TriCo—Triple Co-piloting of Implementation, Specification and Tests

TRICERA: Verifying C Programs Using the Theory of Heaps

Esen, Zafer; Rümmer, Philipp

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

Liang, Chencheng; Rümmer, Philipp; Brockschmidt, Marc

Part of PAAR’22, 2022

• Download full text (pdf) of Exploring Representation of Horn clauses using GNNs

OptiRica: Towards an Efficient Optimizing Horn Solver

Hojjat, Hossein; Rümmer, Philipp

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

Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems: the Case of Aerial Drones

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp

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

Kan, Shuanglong; Lin, Anthony Widjaja; Rümmer, Philipp; Schrader, Micha

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

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp

2022

Towards String Support in JayHorn (Competition Contribution)

Shamakhi, Ali; Hojjat, Hossein; Rümmer, Philipp

Part of Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021, p. 443-447, 2021

• DOI for Towards String Support in JayHorn (Competition Contribution)

Reasoning in the Theory of Heap: Satisfiability and Interpolation

Esen, Zafer; Rümmer, Philipp

Part of LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2020, p. 173-191, 2021

• DOI for Reasoning in the Theory of Heap: Satisfiability and Interpolation

Competition Report: CHC-COMP-21

Fedyukovich, Grigory; Rümmer, Philipp

Part of Electronic Proceedings in Theoretical Computer Science, p. 91-108, 2021

• DOI for Competition Report: CHC-COMP-21
• Download full text (pdf) of Competition Report: CHC-COMP-21

Towards an SMT-LIB theory of heap

Esen, Zafer; Rümmer, Philipp

Part of Proceedings - 8th International Workshop on Verification and Program Transformation, VPT 2020 and 7th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2020, p. 159-162, 2020

• DOI for Towards an SMT-LIB theory of heap

Monadic Decomposition in Integer Linear Arithmetic

Hague, Matthew; Lin, Anthony W.; Rümmer, Philipp; Wu, Zhilin

Part of IJCAR 2020, p. 122-140, 2020

• DOI for Monadic Decomposition in Integer Linear Arithmetic

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Chen, Taolue; Hague, Matthew; He, Jinlong; Hu, Denghang et al.

Part of ATVA 2020, p. 325-342, 2020

• DOI for A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Competition Report: CHC-COMP-20

Rümmer, Philipp

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

• DOI for Competition Report: CHC-COMP-20

JayHorn: A Java Model Checker -: (Competition Contribution)

Kahsai, Temesghen; Rümmer, Philipp; Schäf, Martin

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

Hojjat, Hossein; Rümmer, Philipp; Shamakhi, Ali

Part of Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, p. 19-30, 2019

• DOI for On Strings in Software Model Checking

JayHorn: A Java Model Checker

Rümmer, Philipp

Part of PROCEEDINGS OF THE 21ST WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2019), 2019

• DOI for JayHorn: A Java Model Checker

Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols)

Hong, Chih-Duo; Lin, Anthony W.; Majumdar, Rupak; Rümmer, Philipp

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

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Bui, Phi Diep et al.

Part of Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018

• DOI for Trau: SMT solver for string constraints

Exploring Approximations for Floating-Point Arithmetic using UppSAT

Zeljic, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp

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

Backeman, Peter; Rümmer, Philipp; Zeljic, Aleksandar

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

The ELDARICA Horn Solver

Hojjat, Hossein; Rümmer, Philipp

Part of Formal Methods in Computer Aided Design, p. 158-164, 2018

• DOI for The ELDARICA Horn Solver
• Download full text (pdf) of The ELDARICA Horn Solver

Systematic predicate abstraction using variable roles

Demyanova, Yulia; Rümmer, Philipp; Zuleger, Florian

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

Hojjat, Hossein; Rümmer, Philipp

Part of 2017 19th international symposium on symbolic and numeric algorithms for scientific computing (SYNASC 2017), p. 145-152, 2017

• DOI for Deciding and Interpolating Algebraic Data Types by Reduction

Fair termination for parameterized probabilistic concurrent systems

Lengál, Ondrej; Lin, Anthony W.; Majumdar, Rupak; Rümmer, Philipp

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

Chen, Yu-Fang; Hong, Chih-Duo; Lin, Anthony W.; Rümmer, Philipp

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

Kahsai, Temesghen; Kersten, Rody; Rümmer, Philipp; Schäf, Martin

Part of 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, p. 368-384, 2017

• Download full text (pdf) of Quantified heap invariants for object-oriented programs

Optimizing Horn Solvers for Network Repair

Hojjat, Hossein; Rümmer, Philipp; McClurg, Jedidiah; Cerny, Pavol et al.

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

Zeljic, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp

Part of Theory and Applications of Satisfiability Testing, p. 249-266, 2016

• DOI for Deciding bit-vector formulas with mcSAT

JayHorn: A framework for verifying Java programs

Kahsai, Temesghen; Rümmer, Philipp; Sanchez, Huascar; Schäf, Martin

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

Liveness of randomised parameterised systems under arbitrary schedulers

Lin, Anthony W.; Rümmer, Philipp

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

A Comparative Study of GPUVerify and GKLEE

Panda, Anmol; Rümmer, Philipp; Goveas, Neena

Part of 2016 Fourth International Conference On Parallel, Distributed And Grid Computing (PDGC), p. 112-117, 2016

• DOI for A Comparative Study of GPUVerify and GKLEE

Regular Symmetry Patterns

Lin, Anthony W.; Nguyen, Truong Khanh; Rümmer, Philipp; Sun, Jun

Part of Verification, Model Checking, and Abstract Interpretation, p. 455-475, 2016

• DOI for Regular Symmetry Patterns
• Download full text (pdf) of Regular Symmetry Patterns

Norn: An SMT solver for string constraints

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Holík, Lukás et al.

Part of Computer Aided Verification, p. 462-469, 2015

• DOI for Norn: An SMT solver for string constraints

Free variables and theories: Revisiting rigid E-unification

Backeman, Peter; Rümmer, Philipp

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

Brain, Martin; Tinelli, Cesare; Rümmer, Philipp; Wahl, Thomas

Part of Proc. 22nd Symposium on Computer Arithmetic, p. 160-167, 2015

• DOI for An automatable formal semantics for IEEE-754 floating-point arithmetic

Theorem proving with bounded rigid E-unification

Backeman, Peter; Rümmer, Philipp

Part of Automated Deduction – CADE-25, p. 572-587, 2015

• DOI for Theorem proving with bounded rigid E-unification

Bixie: Finding and understanding inconsistent code

McCarthy, Tim; Rümmer, Philipp; Schäf, Martin

Part of Proc. 37th IEEE/ACM International Conference on Software Engineering, p. 645-648, 2015

• DOI for Bixie: Finding and understanding inconsistent code

Automating regression verification

Felsing, Dennis; Grebing, Sarah; Klebanov, Vladimir; Rümmer, Philipp et al.

Part of Software Engineering & Management 2015, p. 75-76, 2015

Conflict-Directed Graph Coverage

Schwartz-Narbonne, Daniel; Schaef, Martin; Jovanovic, Dejan; Rümmer, Philipp et al.

Part of NASA FORMAL METHODS (NFM 2015), p. 327-342, 2015

• DOI for Conflict-Directed Graph Coverage

Efficient algorithms for bounded rigid E-unification

Backeman, Peter; Rümmer, Philipp

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

Felsing, Dennis; Grebing, Sarah; Klebanov, Vladimir; Rümmer, Philipp et al.

Part of ASE '14 Proceedings of the 29th ACM/IEEE international conference on Automated software engineering, p. 349-360, 2014

• DOI for Automating regression verification

Horn Clauses for Communicating Timed Systems

Hojjat, Hossein; Rümmer, Philipp; Subotic, Pavle; Wang, Yi

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

The Gradual Verifier

Arlt, Stephan; Rubio-Gonzalez, Cindy; Rümmer, Philipp; Schäf, Martin et al.

Part of NASA Formal Methods, p. 313-327, 2014

• DOI for The Gradual Verifier
• Download full text (pdf) of The Gradual Verifier

Approximations for Model Construction

Zeljic, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp

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

Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Chen, Yu-Fang; Holik, Lukas et al.

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

• DOI for String Constraints for Verification

Classifying and Solving Horn Clauses for Verification

Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor

Part of Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), 2013

Exploring Interpolants

Rümmer, Philipp; Subotic, Pavle

Part of Formal Methods in Computer-Aided Design (FMCAD), 2013

Disjunctive Interpolants for Horn-Clause Verification

Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor

Part of Computer Aided Verification, p. 347-363, 2013

• DOI for Disjunctive Interpolants for Horn-Clause Verification

A theory for control-flow graph exploration

Arlt, Stephan; Rümmer, Philipp; Schäf, Martin

Part of Automated Technology for Verification and Analysis, p. 506-515, 2013

• DOI for A theory for control-flow graph exploration

A verification toolkit for numerical transition systems

Hojjat, Hossein; Konecný, Filip; Garnier, Florent; Iosif, Radu et al.

Part of FM 2012, p. 247-251, 2012

• DOI for A verification toolkit for numerical transition systems

E-matching with free variables

Rümmer, Philipp

Part of Logic for Programming, Artificial Intelligence, and Reasoning, p. 359-374, 2012

• DOI for E-matching with free variables

Accelerating interpolants

Hojjat, H.; Iosif, R.; Konečný, F.; Kuncak, V. et al.

Part of Automated Technology for Verification and Analysis, p. 187-202, 2012

• DOI for Accelerating interpolants

Tightening test coverage metrics: A case study in equivalence checking using k-induction

Donaldson, Alastair F.; He, Nannan; Kroening, Daniel; Rümmer, Philipp

Part of Formal Methods for Components and Objects, p. 297-315, 2011

• DOI for Tightening test coverage metrics: A case study in equivalence checking using k-induction

Test-case generation for embedded Simulink via formal concept analysis

He, Nannan; Rümmer, Philipp; Kroening, Daniel

Part of Proc. 48th Design Automation Conference, p. 224-229, 2011

• DOI for Test-case generation for embedded Simulink via formal concept analysis

SCRATCH: a tool for automatic analysis of DMA races

Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp

Part of Proc. 16th ACM Symposium on Principles and Practice of Parallel Programming, p. 311-312, 2011

• DOI for SCRATCH: a tool for automatic analysis of DMA races

Software verification using k-induction

Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel; Rümmer, Philipp

Part of Static Analysis, p. 351-368, 2011

• DOI for Software verification using k-induction

Beyond quantifier-free interpolation in extensions of Presburger arithmetic

Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas

Part of Verification, Model Checking, and Abstract Interpretation, p. 88-102, 2011

• DOI for Beyond quantifier-free interpolation in extensions of Presburger arithmetic

Theoretical Aspects of Software Engineering: 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14–16, 2025, Proceedings

Rümmer, Philipp; Wu, Zhilin

2025

• DOI for Theoretical Aspects of Software Engineering: 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14–16, 2025, Proceedings

Verified Software. Theories, Tools, and Experiments: Revised Selected Papers

Piskac, Ruzica; Rümmer, Philipp

2018

Compiling the Mimosa programming language to RTOS tasks

Huber, Nikolaus; Graf, Susanne; Rümmer, Philipp; Wang, Yi

2025

TUF: Time-bounded Fault Tolerance for Nano-satellites

El Yaacoub, Ahmed; Mottola, Luca; Voigt, Thiemo; Rümmer, Philipp et al.