Philipp Rümmer

Sound and Complete Invariant-Based Heap Encodings

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

Ingår i Proceedings of the ACM on Programming Languages, s. 794-822, 2026

• DOI för Sound and Complete Invariant-Based Heap Encodings
• Ladda ner fulltext (pdf) av Sound and Complete Invariant-Based Heap Encodings

A program instrumentation framework for automatic verification

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

Ingår i Formal methods in system design, 2026

• DOI för A program instrumentation framework for automatic verification
• Ladda ner fulltext (pdf) av A program instrumentation framework for automatic verification

Complementable Normal Form of Parametrized Automata

Alber, Franziska; Rümmer, Philipp

Ingår i IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, s. 1-14, 2026

• DOI för Complementable Normal Form of Parametrized Automata

A New Approach for Showing Termination of Parameterized Transition Systems

Herrmann, Roland; Rümmer, Philipp

Ingår i IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, s. 193-207, 2026

• DOI för 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

s. 48-59, 2025

• DOI för Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO
• Ladda ner fulltext (pdf) av 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

Ingår i Proceedings of the ACM on Programming Languages, s. 794-822, 2026

• DOI för Sound and Complete Invariant-Based Heap Encodings
• Ladda ner fulltext (pdf) av Sound and Complete Invariant-Based Heap Encodings

A program instrumentation framework for automatic verification

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

Ingår i Formal methods in system design, 2026

• DOI för A program instrumentation framework for automatic verification
• Ladda ner fulltext (pdf) av A program instrumentation framework for automatic verification

The Power of Regular Constraint Propagation

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

Ingår i Proceedings of the ACM on Programming Languages, s. 3203-3231, 2025

• DOI för The Power of Regular Constraint Propagation
• Ladda ner fulltext (pdf) av 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

Ingår i IEEE Transactions on Software Engineering, s. 1801-1817, 2025

• DOI för Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

A Constraint Solving Approach to Parikh Images of Regular Languages

Stjerna, Amanda; Rümmer, Philipp

Ingår i Proceedings of the ACM on Programming Languages, 2024

• DOI för A Constraint Solving Approach to Parikh Images of Regular Languages
• Ladda ner fulltext (pdf) av 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

Ingår i ACM Transactions on Embedded Computing Systems, s. 1-27, 2023

• DOI för Scheduling Dynamic Software Updates in Mobile Robots
• Ladda ner fulltext (pdf) av 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.

Ingår i Proceedings of the ACM on Programming Languages, 2022

• DOI för Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
• Ladda ner fulltext (pdf) av 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

Ingår i Formal methods in system design, s. 121-156, 2021

• DOI för Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Ladda ner fulltext (pdf) av 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.

Ingår i Proceedings of the ACM on Programming Languages, 2019

• DOI för Decision procedures for path feasibility of string-manipulating programs with complex operations
• Ladda ner fulltext (pdf) av 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.

Ingår i Proceedings of the ACM on Programming Languages, s. 1-32, 2018

• DOI för String constraints with concatenation and transducers solved efficiently
• Ladda ner fulltext (pdf) av String constraints with concatenation and transducers solved efficiently

Automating regression verification of pointer programs by predicate abstraction

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

Ingår i Formal methods in system design, s. 229-259, 2018

• DOI för Automating regression verification of pointer programs by predicate abstraction
• Ladda ner fulltext (pdf) av 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.

Ingår i SIGPLAN notices, s. 602-617, 2017

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

Preface to special issue on satisfiability modulo theories

Griggio, Alberto; Rümmer, Philipp

Ingår i Formal methods in system design, s. 431-432, 2017

• DOI för Preface to special issue on satisfiability modulo theories

An approximation framework for solvers and decision procedures

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

Ingår i Journal of automated reasoning, s. 127-147, 2017

• DOI för An approximation framework for solvers and decision procedures

Preface, Electronic Proceedings in Theoretical Computer Science. Vol 219

Gallagher, John; Rümmer, Philipp

Ingår i Electronic Proceedings in Theoretical Computer Science, 2016

Guiding Craig interpolation with domain-specific abstractions

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

Ingår i Acta Informatica, s. 387-424, 2016

• DOI för Guiding Craig interpolation with domain-specific abstractions
• Ladda ner fulltext (pdf) av Guiding Craig interpolation with domain-specific abstractions

On recursion-free Horn clauses and Craig interpolation

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

Ingår i Formal methods in system design, s. 1-25, 2015

• DOI för 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.

Ingår i Formal methods in system design, s. 93-120, 2013

• DOI för 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

Ingår i Formal methods in system design, s. 83-113, 2011

• DOI för 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

Ingår i Journal of automated reasoning, s. 341-367, 2011

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

Timing is All You Need

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

Ingår i The Combined Power of Research, Education, and Dissemination, s. 259-279, Springer, 2025

• DOI för 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.

Ingår i Guide to Software Verification with Frama-C, s. 553-582, Springer Nature, 2024

• DOI för An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
• Ladda ner fulltext (pdf) av An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Regular Model Checking Revisited

Lin, Anthony W.; Rümmer, Philipp

Ingår i Model Checking, Synthesis, and Learning, s. 97-114, Springer, 2022

• DOI för Regular Model Checking Revisited

Constraint-based Contract Inference for Deductive Verification

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

Ingår i Deductive Software Verification: Future Perspectives, s. 149-176, Springer Nature, 2020

• DOI för Constraint-based Contract Inference for Deductive Verification

Characterization of simulation by probabilistic testing

Rümmer, Philipp; Yi, Wang

Ingår i Theory and Practice of Formal Methods, s. 360-372, Springer, 2016

• DOI för Characterization of simulation by probabilistic testing

Complementable Normal Form of Parametrized Automata

Alber, Franziska; Rümmer, Philipp

Ingår i IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, s. 1-14, 2026

• DOI för Complementable Normal Form of Parametrized Automata

A New Approach for Showing Termination of Parameterized Transition Systems

Herrmann, Roland; Rümmer, Philipp

Ingår i IMPLEMENTATION AND APPLICATION OF AUTOMATA, CIAA 2025, s. 193-207, 2026

• DOI för 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

s. 48-59, 2025

• DOI för Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO
• Ladda ner fulltext (pdf) av 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.

Ingår i Programming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, s. 217-238, 2025

• DOI för 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.

Ingår i Computer Aided Verification, s. 200-214, 2025

• DOI för 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.

Ingår i Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025, s. 145, 2025

• DOI för OSTRICH2: Solver for Complex String Constraints
• Ladda ner fulltext (pdf) av OSTRICH2: Solver for Complex String Constraints

Arithmetizing Shape Analysis

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

Ingår i Computer Aided Verification, s. 56-80, 2025

• DOI för Arithmetizing Shape Analysis
• Ladda ner fulltext (pdf) av Arithmetizing Shape Analysis

What's Decidable About Arrays With Sums?

Herrmann, Roland; Rümmer, Philipp

Ingår i Proceeding of the Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction,, s. 56-74, 2025

• DOI för 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.

Ingår i Frontiers of Combining Systems (FroCoS 2025), s. 327-345, 2025

• DOI för 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

Ingår i Coordination Models and Languages, s. 90-113, 2025

• DOI för 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

Ingår i Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, s. 42-60, 2025

• DOI för 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

Ingår i HOTMOBILE '24, s. 138-138, 2024

• DOI för Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments
• Ladda ner fulltext (pdf) av 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.

Ingår i Automated Technology for Verification and Analysi, s. 279-301, 2024

• DOI för Guiding Word Equation Solving using Graph Neural Networks

Boosting Constrained Horn Solving by Unsat Core Learning

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 280-302, 2024

• DOI för Boosting Constrained Horn Solving by Unsat Core Learning

An Encoding for CLP Problems in SMT-LIB

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

Ingår i Electronic Proceedings in Theoretical Computer Science, s. 118-130, 2024

• DOI för An Encoding for CLP Problems in SMT-LIB
• Ladda ner fulltext (pdf) av 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 för Timing Analysis of Embedded Software Updates

Automatic Program Instrumentation for Automatic Verification

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

Ingår i CAV 2023, s. 281-304, 2023

• DOI för Automatic Program Instrumentation for Automatic Verification

Decision Procedures for Sequence Theories

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

Ingår i CAV 2023: Computer Aided Verification, s. 18-40, 2023

• DOI för Decision Procedures for Sequence Theories

An Active Learning Approach to Synthesizing Program Contracts

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

Ingår i Software Engineering and Formal Methods, SEFM 2023, s. 126-144, 2023

• DOI för 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

Ingår i AUTOMATED DEDUCTION, CADE 29, s. 170-189, 2023

• DOI för A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
• Ladda ner fulltext (pdf) av 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

Ingår i 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), s. 38-53, 2022

• Ladda ner fulltext (pdf) av An SMT-LIB Theory of Heaps

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

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

Ingår i ISoLA 2022: Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, s. 174-187, 2022

• DOI för TriCo—Triple Co-piloting of Implementation, Specification and Tests

TRICERA: Verifying C Programs Using the Theory of Heaps

Esen, Zafer; Rümmer, Philipp

Ingår i Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, s. 380-391, 2022

• DOI för TRICERA: Verifying C Programs Using the Theory of Heaps
• Ladda ner fulltext (pdf) av TRICERA: Verifying C Programs Using the Theory of Heaps

Exploring Representation of Horn clauses using GNNs

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

Ingår i PAAR’22, 2022

• Ladda ner fulltext (pdf) av Exploring Representation of Horn clauses using GNNs

OptiRica: Towards an Efficient Optimizing Horn Solver

Hojjat, Hossein; Rümmer, Philipp

Ingår i Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, s. 35-43, 2022

• DOI för OptiRica: Towards an Efficient Optimizing Horn Solver
• Ladda ner fulltext (pdf) av 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

Ingår i 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), s. 284-285, 2022

• DOI för Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems: the Case of Aerial Drones
• Ladda ner fulltext (pdf) av 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

Ingår i CPP 2022, s. 210-224, 2022

• DOI för CertiStr: A Certified String Solver
• Ladda ner fulltext (pdf) av 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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021, s. 443-447, 2021

• DOI för Towards String Support in JayHorn (Competition Contribution)

Reasoning in the Theory of Heap: Satisfiability and Interpolation

Esen, Zafer; Rümmer, Philipp

Ingår i LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2020, s. 173-191, 2021

• DOI för Reasoning in the Theory of Heap: Satisfiability and Interpolation

Competition Report: CHC-COMP-21

Fedyukovich, Grigory; Rümmer, Philipp

Ingår i Electronic Proceedings in Theoretical Computer Science, s. 91-108, 2021

• DOI för Competition Report: CHC-COMP-21
• Ladda ner fulltext (pdf) av Competition Report: CHC-COMP-21

Towards an SMT-LIB theory of heap

Esen, Zafer; Rümmer, Philipp

Ingår i Proceedings - 8th International Workshop on Verification and Program Transformation, VPT 2020 and 7th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2020, s. 159-162, 2020

• DOI för Towards an SMT-LIB theory of heap

Monadic Decomposition in Integer Linear Arithmetic

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

Ingår i IJCAR 2020, s. 122-140, 2020

• DOI för 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.

Ingår i ATVA 2020, s. 325-342, 2020

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

Competition Report: CHC-COMP-20

Rümmer, Philipp

Ingår i Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, s. 197-219, 2020

• DOI för Competition Report: CHC-COMP-20

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

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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 214-218, 2019

• DOI för JayHorn: A Java Model Checker -: (Competition Contribution)
• Ladda ner fulltext (pdf) av JayHorn: A Java Model Checker -: (Competition Contribution)

On Strings in Software Model Checking

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

Ingår i Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, s. 19-30, 2019

• DOI för On Strings in Software Model Checking

JayHorn: A Java Model Checker

Rümmer, Philipp

Ingår i PROCEEDINGS OF THE 21ST WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2019), 2019

• DOI för 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

Ingår i Computer Aided Verification. CAV 2019., s. 455-474, 2019

• DOI för Probabilistic Bisimulation for Parameterized Systems: (with Applications to Verifying Anonymous Protocols)
• Ladda ner fulltext (pdf) av 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.

Ingår i Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), 2018

• DOI för Trau: SMT solver for string constraints

Exploring Approximations for Floating-Point Arithmetic using UppSAT

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

Ingår i Automated Reasoning, s. 246-262, 2018

• DOI för Exploring Approximations for Floating-Point Arithmetic using UppSAT
• Ladda ner fulltext (pdf) av Exploring Approximations for Floating-Point Arithmetic using UppSAT

Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction

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

Ingår i Formal Methods in Computer-Aided Design, s. 50-59, 2018

• DOI för Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
• Ladda ner fulltext (pdf) av Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction

The ELDARICA Horn Solver

Hojjat, Hossein; Rümmer, Philipp

Ingår i Formal Methods in Computer Aided Design, s. 158-164, 2018

• DOI för The ELDARICA Horn Solver
• Ladda ner fulltext (pdf) av The ELDARICA Horn Solver

Systematic predicate abstraction using variable roles

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

Ingår i NASA Formal Methods, s. 265-281, 2017

• DOI för Systematic predicate abstraction using variable roles
• Ladda ner fulltext (pdf) av Systematic predicate abstraction using variable roles

Deciding and Interpolating Algebraic Data Types by Reduction

Hojjat, Hossein; Rümmer, Philipp

Ingår i 2017 19th international symposium on symbolic and numeric algorithms for scientific computing (SYNASC 2017), s. 145-152, 2017

• DOI för 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

Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 499-517, 2017

• DOI för Fair termination for parameterized probabilistic concurrent systems
• Ladda ner fulltext (pdf) av 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

Ingår i Proceedings of the 17th International Conference on Formal Methods in Computer-Aided Design, s. 76-83, 2017

• DOI för Learning to prove safety over parameterised concurrent systems
• Ladda ner fulltext (pdf) av 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

Ingår i 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, s. 368-384, 2017

• Ladda ner fulltext (pdf) av Quantified heap invariants for object-oriented programs

Optimizing Horn Solvers for Network Repair

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

Ingår i Proceedings of the 2016 16Th Conference on Formal Methods In Computer-Aided Design (FMCAD 2016), s. 73-80, 2016

Deciding bit-vector formulas with mcSAT

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

Ingår i Theory and Applications of Satisfiability Testing, s. 249-266, 2016

• DOI för Deciding bit-vector formulas with mcSAT

JayHorn: A framework for verifying Java programs

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

Ingår i Computer Aided Verification, s. 352-358, 2016

• DOI för JayHorn: A framework for verifying Java programs
• Ladda ner fulltext (pdf) av JayHorn: A framework for verifying Java programs

Liveness of randomised parameterised systems under arbitrary schedulers

Lin, Anthony W.; Rümmer, Philipp

Ingår i Computer Aided Verification, s. 112-133, 2016

• DOI för Liveness of randomised parameterised systems under arbitrary schedulers
• Ladda ner fulltext (pdf) av Liveness of randomised parameterised systems under arbitrary schedulers

A Comparative Study of GPUVerify and GKLEE

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

Ingår i 2016 Fourth International Conference On Parallel, Distributed And Grid Computing (PDGC), s. 112-117, 2016

• DOI för A Comparative Study of GPUVerify and GKLEE

Regular Symmetry Patterns

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 455-475, 2016

• DOI för Regular Symmetry Patterns
• Ladda ner fulltext (pdf) av 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.

Ingår i Computer Aided Verification, s. 462-469, 2015

• DOI för Norn: An SMT solver for string constraints

Free variables and theories: Revisiting rigid E-unification

Backeman, Peter; Rümmer, Philipp

Ingår i Frontiers of Combining Systems, s. 3-13, 2015

• DOI för Free variables and theories: Revisiting rigid E-unification
• Ladda ner fulltext (pdf) av 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

Ingår i Proc. 22nd Symposium on Computer Arithmetic, s. 160-167, 2015

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

Theorem proving with bounded rigid E-unification

Backeman, Peter; Rümmer, Philipp

Ingår i Automated Deduction – CADE-25, s. 572-587, 2015

• DOI för Theorem proving with bounded rigid E-unification

Bixie: Finding and understanding inconsistent code

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

Ingår i Proc. 37th IEEE/ACM International Conference on Software Engineering, s. 645-648, 2015

• DOI för Bixie: Finding and understanding inconsistent code

Automating regression verification

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

Ingår i Software Engineering & Management 2015, s. 75-76, 2015

Conflict-Directed Graph Coverage

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

Ingår i NASA FORMAL METHODS (NFM 2015), s. 327-342, 2015

• DOI för Conflict-Directed Graph Coverage

Efficient algorithms for bounded rigid E-unification

Backeman, Peter; Rümmer, Philipp

Ingår i Automated Reasoning with Analytic Tableaux and Related Methods, s. 70-85, 2015

• DOI för Efficient algorithms for bounded rigid E-unification
• Ladda ner fulltext (pdf) av Efficient algorithms for bounded rigid E-unification

Automating regression verification

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

Ingår i ASE '14 Proceedings of the 29th ACM/IEEE international conference on Automated software engineering, s. 349-360, 2014

• DOI för Automating regression verification

Horn Clauses for Communicating Timed Systems

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

Ingår i Proceedings First Workshop on Horn Clauses for Verification and Synthesis, s. 39-52, 2014

• DOI för Horn Clauses for Communicating Timed Systems
• Ladda ner fulltext (pdf) av Horn Clauses for Communicating Timed Systems

The Gradual Verifier

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

Ingår i NASA Formal Methods, s. 313-327, 2014

• DOI för The Gradual Verifier
• Ladda ner fulltext (pdf) av The Gradual Verifier

Approximations for Model Construction

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

Ingår i Automated Reasoning, s. 344-359, 2014

• DOI för Approximations for Model Construction
• Ladda ner fulltext (pdf) av Approximations for Model Construction

String Constraints for Verification

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

Ingår i 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, s. 150-166, 2014

• DOI för String Constraints for Verification

Classifying and Solving Horn Clauses for Verification

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

Ingår i Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), 2013

Exploring Interpolants

Rümmer, Philipp; Subotic, Pavle

Ingår i Formal Methods in Computer-Aided Design (FMCAD), 2013

Disjunctive Interpolants for Horn-Clause Verification

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

Ingår i Computer Aided Verification, s. 347-363, 2013

• DOI för Disjunctive Interpolants for Horn-Clause Verification

A theory for control-flow graph exploration

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

Ingår i Automated Technology for Verification and Analysis, s. 506-515, 2013

• DOI för A theory for control-flow graph exploration

A verification toolkit for numerical transition systems

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

Ingår i FM 2012, s. 247-251, 2012

• DOI för A verification toolkit for numerical transition systems

E-matching with free variables

Rümmer, Philipp

Ingår i Logic for Programming, Artificial Intelligence, and Reasoning, s. 359-374, 2012

• DOI för E-matching with free variables

Accelerating interpolants

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

Ingår i Automated Technology for Verification and Analysis, s. 187-202, 2012

• DOI för 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

Ingår i Formal Methods for Components and Objects, s. 297-315, 2011

• DOI för 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

Ingår i Proc. 48th Design Automation Conference, s. 224-229, 2011

• DOI för 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

Ingår i Proc. 16th ACM Symposium on Principles and Practice of Parallel Programming, s. 311-312, 2011

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

Software verification using k-induction

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

Ingår i Static Analysis, s. 351-368, 2011

• DOI för Software verification using k-induction

Beyond quantifier-free interpolation in extensions of Presburger arithmetic

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

Ingår i Verification, Model Checking, and Abstract Interpretation, s. 88-102, 2011

• DOI för Beyond quantifier-free interpolation in extensions of Presburger arithmetic

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.

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

Rümmer, Philipp; Wu, Zhilin

2025

• DOI för 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