Philipp Rümmer

174 papers A* 6A 12B 29C 8Misc 3Journal 58Unranked 50

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A program instrumentation framework for automatic verification. Formal Methods Syst. Des. Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, Marten Voorberg
2026	J	`jnl`	Craig Interpolation in Program Verification. CoRR Philipp Rümmer
2026	J	`jnl`	Synthesis and Verification of Transformer Programs. CoRR Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin
2026	Misc	`ed.`	Theoretical Aspects of Software Engineering - 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14-16, 2025, Proceedings TASE Philipp Rümmer, Zhilin Wu
2025	C	`conf`	A New Approach for Showing Termination of Parameterized Transition Systems. CIAA Roland Herrmann, Philipp Rümmer
2025	—	`conf`	Arithmetizing Shape Analysis. CAV (1) Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies
2025	J	`jnl`	Compiling the Mimosa programming language to RTOS tasks. CoRR Nikolaus Huber, Susanne Graf, Philipp Rümmer, Wang Yi
2025	C	`conf`	Complementable Normal Form of Parametrized Automata. CIAA Franziska Alber, Philipp Rümmer
2025	J	`jnl`	Decision Procedure for A Theory of String Sequences. CoRR Denghang Hu, Taolue Chen, Philipp Rümmer, Fu Song, Zhilin Wu
2025	B	`conf`	Decision Procedure for a Theory of String Sequences. APLAS Denghang Hu, Taolue Chen, Philipp Rümmer, Fu Song, Zhilin Wu
2025	—	`conf`	Finding Universally Quantified Heap Invariants by Horn Clause Transformations. FSEN Zafer Esen, Philipp Rümmer, Tjark Weber
2025	J	`jnl`	HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report). CoRR Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Daniel Stan
2025	C	`conf`	Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software. COORDINATION Nikolaus Huber, Susanne Graf, Philipp Rümmer, Wang Yi
2025	J	`jnl`	Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software. CoRR Nikolaus Huber, Susanne Graf, Philipp Rümmer, Wang Yi
2025	B	`conf`	OSTRICH2: Solver for Complex String Constraints. FMCAD Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu
2025	J	`jnl`	OSTRICH2: Solver for Complex String Constraints. CoRR Matthew Hague, Denghang Hu, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu
2025	J	`jnl`	Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification. CoRR Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar
2025	J	`jnl`	Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification. IEEE Trans. Software Eng. Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar
2025	J	`jnl`	Sound and Complete Invariant-Based Heap Encodings (Technical Report). CoRR Zafer Esen, Philipp Rümmer, Tjark Weber
2025	J	`jnl`	The Power of Regular Constraint Propagation (Technical Report). CoRR Matthew Hague, Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer
2025	J	`jnl`	The Power of Regular Constraint Propagation. Proc. ACM Program. Lang. Matthew Hague, Artur Jez, Anthony Widjaja Lin, Oliver Markgraf, Philipp Rümmer
2025	—	`conf`	Timing is All You Need. The Combined Power of Research, Education, and Dissemination Susanne Graf, Bengt Jonsson, Behnam Khodabandeloo, Chengzi Huang, Nikolaus Huber, Philipp Rümmer, Wang Yi
2025	J	`jnl`	Verification of E-Voting Algorithms in Dafny. CoRR Robert Büttner, Fabian Franz Dießl, Patrick Janoschek, Ivana Kostadinovic, Henrik Oback, Kilian Voß, Franziska Alber, Roland Herrmann, Sibylle Möhle, Philipp Rümmer
2025	A	`conf`	What's Decidable About Arrays With Sums? CADE Roland Herrmann, Philipp Rümmer
2025	J	`jnl`	When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report). CoRR Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer
2025	—	`conf`	When GNNs Met a Word Equations Solver: Learning to Rank Equations. FroCoS Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer
2025	—	`conf`	sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses. CAV (1) Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Daniel Stan
2024	J	`jnl`	A Constraint Solving Approach to Parikh Images of Regular Languages. Proc. ACM Program. Lang. Amanda Stjerna, Philipp Rümmer
2024	J	`jnl`	A Program Instrumentation Framework for Automatic Verification. CoRR Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, Marten Voorberg
2024	J	`jnl`	Arithmetizing Shape Analysis. CoRR Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies
2024	—	`conf`	Boosting Constrained Horn Solving by Unsat Core Learning. VMCAI (1) Parosh Aziz Abdulla, Chencheng Liang, Philipp Rümmer
2024	B	`ed.`	Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024 FMCAD Nina Narodytska, Philipp Rümmer
2024	B	`conf`	Guiding Word Equation Solving Using Graph Neural Networks. ATVA Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer
2024	J	`jnl`	Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report). CoRR Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer
2024	Misc	`conf`	Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments. HotMobile Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2023	A	`conf`	A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). CADE Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai
2023	B	`conf`	An Active Learning Approach to Synthesizing Program Contracts. SEFM Sandip Ghosal, Bengt Jonsson, Philipp Rümmer
2023	—	`conf`	An Encoding for CLP Problems in SMT-LIB. LSFA/HCVS Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer
2023	J	`jnl`	Automatic Program Instrumentation for Automatic Verification (Extended Technical Report). CoRR Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer
2023	—	`conf`	Automatic Program Instrumentation for Automatic Verification. CAV (3) Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer
2023	A*	`conf`	Black Ostrich: Web Application Scanning with String Solvers. CCS Benjamin Eriksson, Amanda Stjerna, Riccardo De Masellis, Philipp Rümmer, Andrei Sabelfeld
2023	J	`jnl`	Decision Procedures for Sequence Theories (Technical Report). CoRR Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer
2023	—	`conf`	Decision Procedures for Sequence Theories. CAV (2) Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer
2023	J	`jnl`	Scheduling Dynamic Software Updates in Mobile Robots. ACM Trans. Embed. Comput. Syst. Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2023	B	`conf`	Timing Analysis of Embedded Software Updates. RTCSA Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2023	J	`jnl`	Timing Analysis of Embedded Software Updates. CoRR Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2022	—	`conf`	Alice in Wineland: A Fairy Tale with Contracts. The Logic of Software. A Tasting Menu of Formal Methods Dilian Gurov, Christian Lidström, Philipp Rümmer
2022	—	`conf`	An SMT-LIB Theory of Heaps. SMT Zafer Esen, Philipp Rümmer
2022	B	`conf`	CertiStr: a certified string solver. CPP Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader
2022	J	`jnl`	Exploring Representation of Horn Clauses using GNNs (Extended Technique Report). CoRR Chencheng Liang, Philipp Rümmer, Marc Brockschmidt
2022	—	`conf`	Exploring Representation of Horn clauses using GNNs. PAAR@IJCAR Chencheng Liang, Philipp Rümmer, Marc Brockschmidt
2022	B	`conf`	NeRTA: Enabling Dynamic Software Updates in Mobile Robotics. EWSN Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2022	—	`conf`	OptiRica: Towards an Efficient Optimizing Horn Solver. HCVS/VPT@ETAPS Hossein Hojjat, Philipp Rümmer
2022	—	`conf`	Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems - the Case of Aerial Drones. ICCPS Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer
2022	J	`jnl`	Solving string constraints with Regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
2022	—	`conf`	TriCo - Triple Co-piloting of Implementation, Specification and Tests. ISoLA (1) Wolfgang Ahrendt, Dilian Gurov, Moa Johansson, Philipp Rümmer
2022	B	`conf`	Tricera: Verifying C Programs Using the Theory of Heaps. FMCAD Zafer Esen, Philipp Rümmer
2021	J	`jnl`	A Theory of Heap for Constrained Horn Clauses (Extended Technical Report). CoRR Zafer Esen, Philipp Rümmer
2021	J	`jnl`	CertiStr: A Certified String Solver (technical report). CoRR Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Micha Schrader
2021	—	`conf`	Competition Report: CHC-COMP-21. HCVS@ETAPS Grigory Fedyukovich, Philipp Rümmer
2021	J	`jnl`	Integrated Deduction (Dagstuhl Seminar 21371). Dagstuhl Reports Maria Paola Bonacina, Philipp Rümmer, Renate A. Schmidt
2021	J	`jnl`	Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic. Formal Methods Syst. Des. Peter Backeman, Philipp Rümmer, Aleksandar Zeljic
2021	—	`conf`	Regular Model Checking Revisited. Model Checking, Synthesis, and Learning Anthony W. Lin, Philipp Rümmer
2021	J	`jnl`	Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. CoRR Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu
2021	—	`conf`	Towards String Support in JayHorn (Competition Contribution). TACAS (2) Ali Shamakhi, Hossein Hojjat, Philipp Rümmer
2020	B	`conf`	A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. ATVA Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu
2020	J	`jnl`	A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. CoRR Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu
2020	—	`conf`	Abstract: Towards an SMT-LIB Theory of Heap. SMT Zafer Esen, Philipp Rümmer
2020	—	`conf`	Competition Report: CHC-COMP-20. VPT/HCVS@ETAPS Philipp Rümmer
2020	—	`ch.`	Constraint-Based Contract Inference for Deductive Verification. 20 Years of KeY Anoud Alshnakat, Dilian Gurov, Christian Lidström, Philipp Rümmer
2020	—	`conf`	Invited Talk: Solving String Constraints, Starting from the Beginning and from the End. SMT Philipp Rümmer
2020	—	`ed.`	Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual). PAAR+SC²@IJCAR Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret
2020	J	`jnl`	Monadic Decomposition in Integer Linear Arithmetic (Technical Report). CoRR Matthew Hague, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu
2020	—	`conf`	Monadic Decomposition in Integer Linear Arithmetic. IJCAR (1) Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
2020	J	`jnl`	Probabilistic Bisimulation for Parameterized Systems (Technical Report). CoRR Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer
2020	C	`conf`	Reasoning in the Theory of Heap: Satisfiability and Interpolation. LOPSTR Zafer Esen, Philipp Rümmer
2020	J	`jnl`	Regular Model Checking Revisited (Technical Report). CoRR Anthony W. Lin, Philipp Rümmer
2020	J	`jnl`	String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). CoRR Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar
2019	J	`jnl`	Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
2019	J	`jnl`	Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). Dagstuhl Reports Carsten Fuhs, Philipp Rümmer, Renate A. Schmidt, Cesare Tinelli
2019	—	`conf`	JayHorn: A Java Model Checker - (Competition Contribution). TACAS (3) Temesghen Kahsai, Philipp Rümmer, Martin Schäf
2019	—	`conf`	JayHorn: a Java model checker. FTfJP@ECOOP Philipp Rümmer
2019	B	`conf`	On Strings in Software Model Checking. APLAS Hossein Hojjat, Philipp Rümmer, Ali Shamakhi
2019	—	`conf`	Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). CAV (1) Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer
2018	J	`jnl`	Automating regression verification of pointer programs by predicate abstraction. Formal Methods Syst. Des. Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
2018	B	`conf`	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. FMCAD Peter Backeman, Philipp Rümmer, Aleksandar Zeljic
2018	J	`jnl`	Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report). CoRR Hossein Hojjat, Philipp Rümmer
2018	J	`jnl`	Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. CoRR Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
2018	A	`conf`	Exploring Approximations for Floating-Point Arithmetic Using UppSAT. IJCAR Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer
2018	—	`ed.`	Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018. PAAR@FLoC Boris Konev, Josef Urban, Philipp Rümmer
2018	J	`jnl`	String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang. Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar
2018	B	`conf`	The ELDARICA Horn Solver. FMCAD Hossein Hojjat, Philipp Rümmer
2018	B	`conf`	Trau: SMT solver for string constraints. FMCAD Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer
2018	—	`ed.`	Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers VSTTE Ruzica Piskac, Philipp Rümmer
2017	—	`conf`	Abduction by Non-Experts. LPAR (Short Presentations) Nikolaj S. Bjørner, Dejan Jovanovic, Tancrède Lepoint, Philipp Rümmer, Martin Schäf
2017	J	`jnl`	An Approximation Framework for Solvers and Decision Procedures. J. Autom. Reason. Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
2017	Misc	`conf`	Deciding and Interpolating Algebraic Data Types by Reduction. SYNASC Hossein Hojjat, Philipp Rümmer
2017	J	`jnl`	Exploring Approximations for Floating-Point Arithmetic using UppSAT. CoRR Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer
2017	J	`jnl`	Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report). CoRR Ondrej Lengál, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer
2017	—	`conf`	Fair Termination for Parameterized Probabilistic Concurrent Systems. TACAS (1) Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rümmer
2017	A*	`conf`	Flatten and conquer: a framework for efficient analysis of string constraints. PLDI Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer
2017	J	`jnl`	Learning to Prove Safety over Parameterised Concurrent Systems (Full Version). CoRR Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer
2017	B	`conf`	Learning to prove safety over parameterised concurrent systems. FMCAD Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer
2017	J	`jnl`	Preface to special issue on satisfiability modulo theories. Formal Methods Syst. Des. Alberto Griggio, Philipp Rümmer
2017	B	`conf`	Quantified Heap Invariants for Object-Oriented Programs. LPAR Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf
2017	—	`conf`	Systematic Predicate Abstraction Using Variable Roles. NFM Yulia Demyanova, Philipp Rümmer, Florian Zuleger
2016	—	`conf`	Characterization of Simulation by Probabilistic Testing. Theory and Practice of Formal Methods Philipp Rümmer, Wang Yi
2016	A	`conf`	Deciding Bit-Vector Formulas with mcSAT. SAT Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
2016	J	`jnl`	Guiding Craig interpolation with domain-specific abstractions. Acta Informatica Jérôme Leroux, Philipp Rümmer, Pavle Subotic
2016	—	`conf`	JayHorn: A Framework for Verifying Java programs. CAV (1) Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez, Martin Schäf
2016	J	`jnl`	Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report). CoRR Anthony W. Lin, Philipp Rümmer
2016	—	`conf`	Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. CAV (2) Anthony W. Lin, Philipp Rümmer
2016	B	`conf`	Optimizing horn solvers for network repair. FMCAD Hossein Hojjat, Philipp Rümmer, Jedidiah McClurg, Pavol Cerný, Nate Foster
2016	—	`ed.`	Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016. HCVS@ETAPS John P. Gallagher, Philipp Rümmer
2016	—	`ch.`	Proof Search with Taclets. Deductive Software Verification Philipp Rümmer, Mattias Ulbrich
2016	B	`conf`	Regular Symmetry Patterns. VMCAI Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun
2015	C	`conf`	An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. ARITH Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
2015	—	`conf`	Automating Regression Verification. Software Engineering & Management Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
2015	—	`conf`	Bixie: Finding and Understanding Inconsistent Code. ICSE (2) Tim McCarthy, Philipp Rümmer, Martin Schäf
2015	—	`conf`	Conflict-Directed Graph Coverage. NFM Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanovic, Philipp Rümmer, Thomas Wies
2015	B	`conf`	Efficient Algorithms for Bounded Rigid E-unification. TABLEAUX Peter Backeman, Philipp Rümmer
2015	—	`conf`	Free Variables and Theories: Revisiting Rigid E-unification. FroCos Peter Backeman, Philipp Rümmer
2015	—	`conf`	Norn: An SMT Solver for String Constraints. CAV (1) Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
2015	J	`jnl`	On recursion-free Horn clauses and Craig interpolation. Formal Methods Syst. Des. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2015	J	`jnl`	Regular Symmetry Patterns (Technical Report). CoRR Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun
2015	A	`conf`	Theorem Proving with Bounded Rigid E-Unification. CADE Peter Backeman, Philipp Rümmer
2014	A	`conf`	Approximations for Model Construction. IJCAR Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
2014	A*	`conf`	Automating regression verification. ASE Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
2014	—	`conf`	Horn Clauses for Communicating Timed Systems. HCVS Hossein Hojjat, Philipp Rümmer, Pavle Subotic, Wang Yi
2014	—	`ed.`	Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, affiliated with the 26th International Conference on Computer Aided Verification (CAV 2014), the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), and the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria, July 17-18, 2014. SMT Philipp Rümmer, Christoph M. Wintersteiger
2014	A*	`conf`	String Constraints for Verification. CAV Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
2014	—	`conf`	The Gradual Verifier. NASA Formal Methods Stephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf, Natarajan Shankar
2013	B	`conf`	A Theory for Control-Flow Graph Exploration. ATVA Stephan Arlt, Philipp Rümmer, Martin Schäf
2013	—	`conf`	Classifying and Solving Horn Clauses for Verification. VSTTE Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	J	`jnl`	Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report) CoRR Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	A*	`conf`	Disjunctive Interpolants for Horn-Clause Verification. CAV Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2013	B	`conf`	Exploring interpolants. FMCAD Philipp Rümmer, Pavle Subotic
2013	—	`conf`	Joogie: from Java through Jimple to Boogie. SOAP@PLDI Stephan Arlt, Philipp Rümmer, Martin Schäf
2013	J	`jnl`	Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2013	J	`jnl`	The Relationship between Craig Interpolation and Recursion-Free Horn Clauses CoRR Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
2012	B	`conf`	A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer
2012	B	`conf`	Accelerating Interpolants. ATVA Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer
2012	—	`conf`	Craig Interpolation for the Integers: Results, Implementation, and Experiences. IWIL@LPAR Philipp Rümmer
2012	B	`conf`	E-Matching with Free Variables. LPAR Philipp Rümmer
2011	J	`jnl`	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reason. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2011	J	`jnl`	Automatic analysis of DMA races using model checking and Formal Methods Syst. Des. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2011	B	`conf`	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. VMCAI Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2011	B	`conf`	SCRATCH: a tool for automatic analysis of dma races. PPoPP Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2011	B	`conf`	Software Verification Using k-Induction. SAS Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer
2011	A*	`conf`	Test-case generation for embedded simulink via formal concept analysis. DAC Nannan He, Philipp Rümmer, Daniel Kroening
2010	A	`conf`	A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS K. Rustan M. Leino, Philipp Rümmer
2010	A	`conf`	An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. IJCAR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	A	`conf`	Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. TACAS Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
2010	J	`jnl`	Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report) CoRR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	—	`conf`	Interpolating Quantifier-Free Presburger Arithmetic. LPAR (Yogyakarta) Daniel Kroening, Jérôme Leroux, Philipp Rümmer
2010	J	`jnl`	Practical Aspects of Automated Deduction for Program Verification. Künstliche Intell. Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer
2010	—	`conf`	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. VERIFY@IJCAR Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
2010	A	`conf`	Ranking Function Synthesis for Bit-Vector Relations. TACAS Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
2010	—	`conf`	Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction. FMCO Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer
2009	—	`conf`	Mutation-Based Test Case Generation for Simulink Models. FMCO Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher
2009	A	`conf`	Real World Verification. CADE André Platzer, Jan-David Quesel, Philipp Rümmer
2008	B	`conf`	A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. LPAR Philipp Rümmer
2008	C	`conf`	Integrating Verification and Testing of Object-Oriented Software. TAP Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer
2008	J	`jnl`	Integration of a security type system into a program logic. Theor. Comput. Sci. Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
2008	C	`conf`	Non-termination Checking for Imperative Programs. TAP Helga Velroyen, Philipp Rümmer
2007	—	`conf`	A Sequent Calculus for Integer Arithmetic with Counterexample Generation. VERIFY Philipp Rümmer
2007	—	`ch.`	Construction of Proofs. The KeY Approach Philipp Rümmer
2007	C	`conf`	Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic. TAP Philipp Rümmer, Muhammad Ali Shah
2007	A	`conf`	The KeY system 1.0 (Deduction Component). CADE Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
2006	—	`conf`	Integration of a Security Type System into a Program Logic. TGC Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
2006	B	`conf`	Sequential, Parallel, and Quantified Updates of First-Order Structures. LPAR Philipp Rümmer
2006	—	`conf`	Verifying Object-Oriented Programs with KeY: A Tutorial. FMCO Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt
2005	—	`conf`	Verification of JCSP Programs. CPA Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
2004	—	`conf`	Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. LFM@IJCAR Richard Bubel, Andreas Roth, Philipp Rümmer