| 2025 | APLAS | Decision Procedure for a Theory of String Sequences. | Denghang Hu, Taolue Chen, Philipp Rmmer, Fu Song, Zhilin Wu |
| 2025 | CADE | What's Decidable About Arrays With Sums? | Roland Herrmann, Philipp Rmmer |
| 2025 | CAV | sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses. | Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Philipp Rmmer, Daniel Stan |
| 2025 | CAV | Arithmetizing Shape Analysis. | Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rmmer, Thomas Wies |
| 2025 | Coordination | Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software. | Nikolaus Huber, Susanne Graf, Philipp Rmmer, Wang Yi |
| 2025 | EWSN | Fault Tolerance in Space with Heterogeneous Hardware: Experiences from a 68-day CubeSat Deployment in LEO. | Ahmed El Yaacoub, Thiemo Voigt, Philipp Rmmer, Luca Mottola |
| 2025 | FMCAD | OSTRICH2: Solver for Complex String Constraints. | Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rmmer, Zhilin Wu |
| 2024 | ATVA | Guiding Word Equation Solving Using Graph Neural Networks. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rmmer |
| 2024 | VMCAI | Boosting Constrained Horn Solving by Unsat Core Learning. | Parosh Aziz Abdulla, Chencheng Liang, Philipp Rmmer |
| 2023 | CADE | A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). | Yu-Fang Chen, Philipp Rmmer, Wei-Lun Tsai |
| 2023 | CAV | Automatic Program Instrumentation for Automatic Verification. | Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidstrm, Philipp Rmmer |
| 2023 | CAV | Decision Procedures for Sequence Theories. | Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rmmer |
| 2023 | CCS | Black Ostrich: Web Application Scanning with String Solvers. | Benjamin Eriksson, Amanda Stjerna, Riccardo De Masellis, Philipp Rmmer, Andrei Sabelfeld |
| 2023 | RTCSA | Timing Analysis of Embedded Software Updates. | Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rmmer |
| 2023 | SEFM | An Active Learning Approach to Synthesizing Program Contracts. | Sandip Ghosal, Bengt Jonsson, Philipp Rmmer |
| 2022 | CPP | CertiStr: a certified string solver. | Shuanglong Kan, Anthony Widjaja Lin, Philipp Rmmer, Micha Schrader |
| 2022 | EWSN | NeRTA: Enabling Dynamic Software Updates in Mobile Robotics. | Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rmmer |
| 2022 | FMCAD | Tricera: Verifying C Programs Using the Theory of Heaps. | Zafer Esen, Philipp Rmmer |
| 2022 | ISoLA | TriCo - Triple Co-piloting of Implementation, Specification and Tests. | Wolfgang Ahrendt, Dilian Gurov, Moa Johansson, Philipp Rmmer |
| 2021 | TACAS | Towards String Support in JayHorn (Competition Contribution). | Ali Shamakhi, Hossein Hojjat, Philipp Rmmer |
| 2020 | ATVA | A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. | Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rmmer, Zhilin Wu |
| 2020 | CADE | Monadic Decomposition in Integer Linear Arithmetic. | Matthew Hague, Anthony W. Lin, Philipp Rmmer, Zhilin Wu |
| 2020 | LOPSTR | Reasoning in the Theory of Heap: Satisfiability and Interpolation. | Zafer Esen, Philipp Rmmer |
| 2019 | APLAS | On Strings in Software Model Checking. | Hossein Hojjat, Philipp Rmmer, Ali Shamakhi |
| 2019 | CAV | Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). | Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rmmer |
| 2019 | ECOOP | JayHorn: a Java model checker. | Philipp Rmmer |
| 2019 | TACAS | JayHorn: A Java Model Checker - (Competition Contribution). | Temesghen Kahsai, Philipp Rmmer, Martin Schf |
| 2018 | CADE | Exploring Approximations for Floating-Point Arithmetic Using UppSAT. | Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rmmer |
| 2018 | FMCAD | Trau: SMT solver for string constraints. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luks Holk, Ahmed Rezine, Philipp Rmmer |
| 2018 | FMCAD | Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. | Peter Backeman, Philipp Rmmer, Aleksandar Zeljic |
| 2018 | FMCAD | The ELDARICA Horn Solver. | Hossein Hojjat, Philipp Rmmer |
| 2017 | FMCAD | Learning to prove safety over parameterised concurrent systems. | Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rmmer |
| 2017 | LPAR | Abduction by Non-Experts. | Nikolaj S. Bjrner, Dejan Jovanovic, Tancrde Lepoint, Philipp Rmmer, Martin Schf |
| 2017 | LPAR | Quantified Heap Invariants for Object-Oriented Programs. | Temesghen Kahsai, Rody Kersten, Philipp Rmmer, Martin Schf |
| 2017 | PLDI | Flatten and conquer: a framework for efficient analysis of string constraints. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luks Holk, Ahmed Rezine, Philipp Rmmer |
| 2017 | SYNASC | Deciding and Interpolating Algebraic Data Types by Reduction. | Hossein Hojjat, Philipp Rmmer |
| 2017 | TACAS | Fair Termination for Parameterized Probabilistic Concurrent Systems. | Ondrej Lengl, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rmmer |
| 2016 | CAV | JayHorn: A Framework for Verifying Java programs. | Temesghen Kahsai, Philipp Rmmer, Huascar Sanchez, Martin Schf |
| 2016 | CAV | Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. | Anthony W. Lin, Philipp Rmmer |
| 2016 | FMCAD | Optimizing horn solvers for network repair. | Hossein Hojjat, Philipp Rmmer, Jedidiah McClurg, Pavol Cern, Nate Foster |
| 2016 | SAT | Deciding Bit-Vector Formulas with mcSAT. | Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rmmer |
| 2016 | VMCAI | Regular Symmetry Patterns. | Anthony W. Lin, Truong Khanh Nguyen, Philipp Rmmer, Jun Sun |
| 2015 | ARITH | An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. | Martin Brain, Cesare Tinelli, Philipp Rmmer, Thomas Wahl |
| 2015 | CADE | Theorem Proving with Bounded Rigid E-Unification. | Peter Backeman, Philipp Rmmer |
| 2015 | CAV | Norn: An SMT Solver for String Constraints. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Luks Holk, Ahmed Rezine, Philipp Rmmer, Jari Stenman |
| 2015 | ICSE | Bixie: Finding and Understanding Inconsistent Code. | Tim McCarthy, Philipp Rmmer, Martin Schf |
| 2015 | TABLEAUX | Efficient Algorithms for Bounded Rigid E-unification. | Peter Backeman, Philipp Rmmer |
| 2014 | CADE | Approximations for Model Construction. | Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rmmer |
| 2014 | CAV | String Constraints for Verification. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Luks Holk, Ahmed Rezine, Philipp Rmmer, Jari Stenman |
| 2013 | ATVA | A Theory for Control-Flow Graph Exploration. | Stephan Arlt, Philipp Rmmer, Martin Schf |
| 2013 | CAV | Disjunctive Interpolants for Horn-Clause Verification. | Philipp Rmmer, Hossein Hojjat, Viktor Kuncak |
| 2013 | FMCAD | Exploring interpolants. | Philipp Rmmer, Pavle Subotic |
| 2013 | PLDI | Joogie: from Java through Jimple to Boogie. | Stephan Arlt, Philipp Rmmer, Martin Schf |
| 2012 | ATVA | Accelerating Interpolants. | Hossein Hojjat, Radu Iosif, Filip Konecn, Viktor Kuncak, Philipp Rmmer |
| 2012 | FM | A Verification Toolkit for Numerical Transition Systems - Tool Paper. | Hossein Hojjat, Filip Konecn, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rmmer |
| 2012 | LPAR | E-Matching with Free Variables. | Philipp Rmmer |
| 2012 | LPAR | Craig Interpolation for the Integers: Results, Implementation, and Experiences. | Philipp Rmmer |
| 2011 | DAC | Test-case generation for embedded simulink via formal concept analysis. | Nannan He, Philipp Rmmer, Daniel Kroening |
| 2011 | PPoPP | SCRATCH: a tool for automatic analysis of dma races. | Alastair F. Donaldson, Daniel Kroening, Philipp Rmmer |
| 2011 | SAS | Software Verification Using k-Induction. | Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rmmer |
| 2011 | VMCAI | Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | LPAR | Interpolating Quantifier-Free Presburger Arithmetic. | Daniel Kroening, Jrme Leroux, Philipp Rmmer |
| 2010 | TACAS | Ranking Function Synthesis for Bit-Vector Relations. | Byron Cook, Daniel Kroening, Philipp Rmmer, Christoph M. Wintersteiger |
| 2010 | TACAS | Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. | Alastair F. Donaldson, Daniel Kroening, Philipp Rmmer |
| 2010 | TACAS | A Polymorphic Intermediate Verification Language: Design and Logical Encoding. | K. Rustan M. Leino, Philipp Rmmer |
| 2009 | CADE | Real World Verification. | Andr Platzer, Jan-David Quesel, Philipp Rmmer |
| 2008 | LPAR | A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. | Philipp Rmmer |
| 2008 | TAP | Integrating Verification and Testing of Object-Oriented Software. | Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rmmer |
| 2008 | TAP | Non-termination Checking for Imperative Programs. | Helga Velroyen, Philipp Rmmer |
| 2007 | CADE | The KeY system 1.0 (Deduction Component). | Bernhard Beckert, Martin Giese, Reiner Hhnle, Vladimir Klebanov, Philipp Rmmer, Steffen Schlager, Peter H. Schmitt |
| 2007 | CADE | A Sequent Calculus for Integer Arithmetic with Counterexample Generation. | Philipp Rmmer |
| 2007 | TAP | Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic. | Philipp Rmmer, Muhammad Ali Shah |
| 2006 | LPAR | Sequential, Parallel, and Quantified Updates of First-Order Structures. | Philipp Rmmer |