Philipp Rümmer

Part of Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, p. 200-214, 2025

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

What's Decidable About Arrays With Sums?

Herrmann, Roland; Rümmer, Philipp

Part of Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, p. 56-74, 2025

DOI for What's Decidable About Arrays With Sums?

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

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

2025

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

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

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

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

Timing Analysis of Embedded Software Updates

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

2023

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

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

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

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

CertiStr: A Certified String Solver

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

Part of CPP 2022, p. 210-224, 2022

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

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

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

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

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

The ELDARICA Horn Solver

Hojjat, Hossein; Rümmer, Philipp

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

Systematic predicate abstraction using variable roles

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

Part of NASA Formal Methods, p. 265-281, 2017

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

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

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

Liveness of randomised parameterised systems under arbitrary schedulers

Lin, Anthony W.; Rümmer, Philipp

Part of Computer Aided Verification, p. 112-133, 2016

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

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

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

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

Free variables and theories: Revisiting rigid E-unification

Backeman, Peter; Rümmer, Philipp

Part of Frontiers of Combining Systems, p. 3-13, 2015

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

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

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

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

Approximations for Model Construction

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

Part of Automated Reasoning, p. 344-359, 2014

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