default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDPhilipp Rümmer
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
[c96]Susanne Graf, Bengt Jonsson, Behnam Khodabandeloo, Chengzi Huang, Nikolaus Huber, Philipp Rümmer, Wang Yi:
Timing is All You Need. The Combined Power of Research, Education, and Dissemination 2025: 259-279- 2024
- [j16]Amanda Stjerna
, Philipp Rümmer:
A Constraint Solving Approach to Parikh Images of Regular Languages. Proc. ACM Program. Lang. 8(OOPSLA1): 1235-1263 (2024) - [c95]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer:
Guiding Word Equation Solving Using Graph Neural Networks. ATVA 2024: 279-301 - [c94]Parosh Aziz Abdulla, Chencheng Liang, Philipp Rümmer:
Boosting Constrained Horn Solving by Unsat Core Learning. VMCAI (1) 2024: 280-302 - [c93]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
Poster: Fault Tolerance with Time Guarantees in Mobile Systems for Extreme Environments. HotMobile 2024: 138 - [i27]Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies:
Arithmetizing Shape Analysis. CoRR abs/2408.09037 (2024) - [i26]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Julie Cailler, Chencheng Liang, Philipp Rümmer:
Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report). CoRR abs/2411.15194 (2024) - [i25]Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, Marten Voorberg:
A Program Instrumentation Framework for Automatic Verification. CoRR abs/2412.06431 (2024) - 2023
- [j15]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
Scheduling Dynamic Software Updates in Mobile Robots. ACM Trans. Embed. Comput. Syst. 22(6): 99:1-99:27 (2023) - [c92]Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai:
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). CADE 2023: 170-189 - [c91]Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer:
Decision Procedures for Sequence Theories. CAV (2) 2023: 18-40 - [c90]Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer:
Automatic Program Instrumentation for Automatic Verification. CAV (3) 2023: 281-304 - [c89]Benjamin Eriksson, Amanda Stjerna, Riccardo De Masellis, Philipp Rümmer, Andrei Sabelfeld:
Black Ostrich: Web Application Scanning with String Solvers. CCS 2023: 549-563 - [c88]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
Timing Analysis of Embedded Software Updates. RTCSA 2023: 1-11 - [c87]Sandip Ghosal, Bengt Jonsson, Philipp Rümmer:
An Active Learning Approach to Synthesizing Program Contracts. SEFM 2023: 126-144 - [c86]Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer:
An Encoding for CLP Problems in SMT-LIB. LSFA/HCVS 2023: 118-130 - [i24]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
Timing Analysis of Embedded Software Updates. CoRR abs/2304.14213 (2023) - [i23]Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer:
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report). CoRR abs/2306.00004 (2023) - [i22]Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer:
Decision Procedures for Sequence Theories (Technical Report). CoRR abs/2308.00175 (2023) - 2022
- [j14]Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Zhilin Wu:
Solving string constraints with Regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [c85]Dilian Gurov, Christian Lidström, Philipp Rümmer:
Alice in Wineland: A Fairy Tale with Contracts. The Logic of Software. A Tasting Menu of Formal Methods 2022: 229-242 - [c84]Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader:
CertiStr: a certified string solver. CPP 2022: 210-224 - [c83]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
NeRTA: Enabling Dynamic Software Updates in Mobile Robotics. EWSN 2022: 120-125 - [c82]Zafer Esen, Philipp Rümmer:
Tricera: Verifying C Programs Using the Theory of Heaps. FMCAD 2022: 380-391 - [c81]Ahmed El Yaacoub, Luca Mottola, Thiemo Voigt, Philipp Rümmer:
Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems - the Case of Aerial Drones. ICCPS 2022: 284-285 - [c80]Wolfgang Ahrendt, Dilian Gurov, Moa Johansson, Philipp Rümmer:
TriCo - Triple Co-piloting of Implementation, Specification and Tests. ISoLA (1) 2022: 174-187 - [c79]Chencheng Liang, Philipp Rümmer, Marc Brockschmidt:
Exploring Representation of Horn clauses using GNNs. PAAR@IJCAR 2022 - [c78]Zafer Esen, Philipp Rümmer:
An SMT-LIB Theory of Heaps. SMT 2022: 38-53 - [c77]Hossein Hojjat, Philipp Rümmer:
OptiRica: Towards an Efficient Optimizing Horn Solver. HCVS/VPT@ETAPS 2022: 35-43 - [i21]Chencheng Liang, Philipp Rümmer, Marc Brockschmidt:
Exploring Representation of Horn Clauses using GNNs (Extended Technique Report). CoRR abs/2206.06986 (2022) - 2021
- [j13]Peter Backeman, Philipp Rümmer, Aleksandar Zeljic:
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic. Formal Methods Syst. Des. 57(2): 121-156 (2021) - [c76]Anthony W. Lin, Philipp Rümmer:
Regular Model Checking Revisited. Model Checking, Synthesis, and Learning 2021: 97-114 - [c75]Ali Shamakhi, Hossein Hojjat, Philipp Rümmer:
Towards String Support in JayHorn (Competition Contribution). TACAS (2) 2021: 443-447 - [c74]Grigory Fedyukovich, Philipp Rümmer:
Competition Report: CHC-COMP-21. HCVS@ETAPS 2021: 91-108 - [i20]Zafer Esen, Philipp Rümmer:
A Theory of Heap for Constrained Horn Clauses (Extended Technical Report). CoRR abs/2104.04224 (2021) - [i19]Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu:
Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. CoRR abs/2111.04298 (2021) - [i18]Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Micha Schrader:
CertiStr: A Certified String Solver (technical report). CoRR abs/2112.06039 (2021) - [i17]Maria Paola Bonacina, Philipp Rümmer, Renate A. Schmidt:
Integrated Deduction (Dagstuhl Seminar 21371). Dagstuhl Reports 11(8): 35-51 (2021) - 2020
- [c73]Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu:
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. ATVA 2020: 325-342 - [c72]Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu:
Monadic Decomposition in Integer Linear Arithmetic. IJCAR (1) 2020: 122-140 - [c71]Zafer Esen, Philipp Rümmer:
Reasoning in the Theory of Heap: Satisfiability and Interpolation. LOPSTR 2020: 173-191 - [c70]Philipp Rümmer:
Invited Talk: Solving String Constraints, Starting from the Beginning and from the End. SMT 2020: 1 - [c69]Zafer Esen, Philipp Rümmer:
Abstract: Towards an SMT-LIB Theory of Heap. SMT 2020: 60 - [c68]Philipp Rümmer:
Competition Report: CHC-COMP-20. VPT/HCVS@ETAPS 2020: 197-219 - [p3]Anoud Alshnakat, Dilian Gurov, Christian Lidström, Philipp Rümmer:
Constraint-Based Contract Inference for Deductive Verification. 20 Years of KeY 2020: 149-176 - [e5]Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret:
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). CEUR Workshop Proceedings 2752, CEUR-WS.org 2020 [contents] - [i16]Matthew Hague, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu:
Monadic Decomposition in Integer Linear Arithmetic (Technical Report). CoRR abs/2004.12371 (2020) - [i15]Anthony W. Lin, Philipp Rümmer:
Regular Model Checking Revisited (Technical Report). CoRR abs/2005.00990 (2020) - [i14]Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, Zhilin Wu:
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. CoRR abs/2007.06913 (2020) - [i13]Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar:
String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). CoRR abs/2010.15975 (2020) - [i12]Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer:
Probabilistic Bisimulation for Parameterized Systems (Technical Report). CoRR abs/2011.02413 (2020)
2010 – 2019
- 2019
- [j12]Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu:
Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL): 49:1-49:30 (2019) - [c67]Hossein Hojjat, Philipp Rümmer, Ali Shamakhi:
On Strings in Software Model Checking. APLAS 2019: 19-30 - [c66]Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer:
Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). CAV (1) 2019: 455-474 - [c65]Philipp Rümmer:
JayHorn: a Java model checker. FTfJP@ECOOP 2019: 1:1 - [c64]Temesghen Kahsai, Philipp Rümmer, Martin Schäf:
JayHorn: A Java Model Checker - (Competition Contribution). TACAS (3) 2019: 214-218 - [i11]Carsten Fuhs, Philipp Rümmer, Renate A. Schmidt, Cesare Tinelli:
Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). Dagstuhl Reports 9(9): 23-44 (2019) - 2018
- [j11]Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich:
Automating regression verification of pointer programs by predicate abstraction. Formal Methods Syst. Des. 52(3): 229-259 (2018) - [j10]Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar:
String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang. 2(POPL): 4:1-4:32 (2018) - [c63]Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer:
Exploring Approximations for Floating-Point Arithmetic Using UppSAT. IJCAR 2018: 246-262 - [c62]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer:
Trau: SMT solver for string constraints. FMCAD 2018: 1-5 - [c61]Peter Backeman, Philipp Rümmer, Aleksandar Zeljic:
Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. FMCAD 2018: 1-10 - [c60]Hossein Hojjat, Philipp Rümmer:
The ELDARICA Horn Solver. FMCAD 2018: 1-7 - [e4]Boris Konev, Josef Urban, Philipp Rümmer:
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. CEUR Workshop Proceedings 2162, CEUR-WS.org 2018 [contents] - [e3]Ruzica Piskac, Philipp Rümmer:
Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers. Lecture Notes in Computer Science 11294, Springer 2018, ISBN 978-3-030-03591-4 [contents] - [i10]Hossein Hojjat, Philipp Rümmer:
Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report). CoRR abs/1801.02367 (2018) - [i9]Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu:
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. CoRR abs/1811.03167 (2018) - 2017
- [j9]Alberto Griggio, Philipp Rümmer:
Preface to special issue on satisfiability modulo theories. Formal Methods Syst. Des. 51(3): 431-432 (2017) - [j8]Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer:
An Approximation Framework for Solvers and Decision Procedures. J. Autom. Reason. 58(1): 127-147 (2017) - [c59]Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer:
Learning to prove safety over parameterised concurrent systems. FMCAD 2017: 76-83 - [c58]Nikolaj S. Bjørner, Dejan Jovanovic, Tancrède Lepoint, Philipp Rümmer, Martin Schäf:
Abduction by Non-Experts. LPAR (Short Presentations) 2017: 58-72 - [c57]Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf:
Quantified Heap Invariants for Object-Oriented Programs. LPAR 2017: 368-384 - [c56]Yulia Demyanova, Philipp Rümmer, Florian Zuleger:
Systematic Predicate Abstraction Using Variable Roles. NFM 2017: 265-281 - [c55]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer:
Flatten and conquer: a framework for efficient analysis of string constraints. PLDI 2017: 602-617 - [c54]Hossein Hojjat, Philipp Rümmer:
Deciding and Interpolating Algebraic Data Types by Reduction. SYNASC 2017: 145-152 - [c53]Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rümmer:
Fair Termination for Parameterized Probabilistic Concurrent Systems. TACAS (1) 2017: 499-517 - [i8]Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer:
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version). CoRR abs/1709.07139 (2017) - [i7]Ondrej Lengál, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer:
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report). CoRR abs/1710.10756 (2017) - [i6]Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer:
Exploring Approximations for Floating-Point Arithmetic using UppSAT. CoRR abs/1711.08859 (2017) - 2016
- [j7]Jérôme Leroux, Philipp Rümmer, Pavle Subotic:
Guiding Craig interpolation with domain-specific abstractions. Acta Informatica 53(4): 387-424 (2016) - [c52]Philipp Rümmer, Wang Yi:
Characterization of Simulation by Probabilistic Testing. Theory and Practice of Formal Methods 2016: 360-372 - [c51]Anthony W. Lin, Philipp Rümmer:
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. CAV (2) 2016: 112-133 - [c50]Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez, Martin Schäf:
JayHorn: A Framework for Verifying Java programs. CAV (1) 2016: 352-358 - [c49]Hossein Hojjat, Philipp Rümmer, Jedidiah McClurg, Pavol Cerný, Nate Foster:
Optimizing horn solvers for network repair. FMCAD 2016: 73-80 - [c48]Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer:
Deciding Bit-Vector Formulas with mcSAT. SAT 2016: 249-266 - [c47]Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun:
Regular Symmetry Patterns. VMCAI 2016: 455-475 - [p2]Philipp Rümmer, Mattias Ulbrich:
Proof Search with Taclets. Deductive Software Verification 2016: 107-147 - [e2]John P. Gallagher, Philipp Rümmer:
Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016. EPTCS 219, 2016 [contents] - [i5]Anthony W. Lin, Philipp Rümmer:
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report). CoRR abs/1606.01451 (2016) - 2015
- [j6]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
On recursion-free Horn clauses and Craig interpolation. Formal Methods Syst. Des. 47(1): 1-25 (2015) - [c46]Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl:
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. ARITH 2015: 160-167 - [c45]Peter Backeman, Philipp Rümmer:
Theorem Proving with Bounded Rigid E-Unification. CADE 2015: 572-587 - [c44]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman:
Norn: An SMT Solver for String Constraints. CAV (1) 2015: 462-469 - [c43]Peter Backeman, Philipp Rümmer:
Free Variables and Theories: Revisiting Rigid E-unification. FroCos 2015: 3-13 - [c42]Tim McCarthy, Philipp Rümmer, Martin Schäf:
Bixie: Finding and Understanding Inconsistent Code. ICSE (2) 2015: 645-648 - [c41]Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanovic, Philipp Rümmer, Thomas Wies:
Conflict-Directed Graph Coverage. NFM 2015: 327-342 - [c40]Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich:
Automating Regression Verification. Software Engineering & Management 2015: 75-76 - [c39]Peter Backeman, Philipp Rümmer:
Efficient Algorithms for Bounded Rigid E-unification. TABLEAUX 2015: 70-85 - [i4]Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun:
Regular Symmetry Patterns (Technical Report). CoRR abs/1510.08506 (2015) - 2014
- [c38]Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer:
Approximations for Model Construction. IJCAR 2014: 344-359 - [c37]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman:
String Constraints for Verification. CAV 2014: 150-166 - [c36]Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich:
Automating regression verification. ASE 2014: 349-360 - [c35]Stephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf, Natarajan Shankar:
The Gradual Verifier. NASA Formal Methods 2014: 313-327 - [c34]Hossein Hojjat, Philipp Rümmer, Pavle Subotic, Wang Yi:
Horn Clauses for Communicating Timed Systems. HCVS 2014: 39-52 - [e1]Philipp Rümmer, Christoph M. Wintersteiger:
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. CEUR Workshop Proceedings 1163, CEUR-WS.org 2014 [contents] - 2013
- [j5]Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger:
Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1): 93-120 (2013) - [c33]Stephan Arlt, Philipp Rümmer, Martin Schäf:
A Theory for Control-Flow Graph Exploration. ATVA 2013: 506-515 - [c32]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Disjunctive Interpolants for Horn-Clause Verification. CAV 2013: 347-363 - [c31]Philipp Rümmer, Pavle Subotic:
Exploring interpolants. FMCAD 2013: 69-76 - [c30]Stephan Arlt, Philipp Rümmer, Martin Schäf:
Joogie: from Java through Jimple to Boogie. SOAP@PLDI 2013: 3-8 - [c29]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Classifying and Solving Horn Clauses for Verification. VSTTE 2013: 1-21 - [i3]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report). CoRR abs/1301.4973 (2013) - [i2]Philipp Rümmer, Hossein Hojjat, Viktor Kuncak:
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses. CoRR abs/1302.4187 (2013) - 2012
- [c28]Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer:
Accelerating Interpolants. ATVA 2012: 187-202 - [c27]Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer:
A Verification Toolkit for Numerical Transition Systems - Tool Paper. FM 2012: 247-251 - [c26]Philipp Rümmer:
Craig Interpolation for the Integers: Results, Implementation, and Experiences. IWIL@LPAR 2012: 3 - [c25]Philipp Rümmer:
E-Matching with Free Variables. LPAR 2012: 359-374 - 2011
- [j4]Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer:
Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des. 39(1): 83-113 (2011) - [j3]Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reason. 47(4): 341-367 (2011) - [c24]Nannan He, Philipp Rümmer, Daniel Kroening:
Test-case generation for embedded simulink via formal concept analysis. DAC 2011: 224-229 - [c23]Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer:
SCRATCH: a tool for automatic analysis of dma races. PPoPP 2011: 311-312 - [c22]Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer:
Software Verification Using k-Induction. SAS 2011: 351-368 - [c21]Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. VMCAI 2011: 88-102 - 2010
- [j2]Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer:
Practical Aspects of Automated Deduction for Program Verification. Künstliche Intell. 24(1): 43-49 (2010) - [c20]Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. VERIFY@IJCAR 2010: 31-46 - [c19]Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. IJCAR 2010: 384-399 - [c18]Alastair F. Donaldson, Nannan He, Daniel Kroening, Philipp Rümmer:
Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction. FMCO 2010: 297-315 - [c17]Daniel Kroening, Jérôme Leroux, Philipp Rümmer:
Interpolating Quantifier-Free Presburger Arithmetic. LPAR (Yogyakarta) 2010: 489-503 - [c16]Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger:
Ranking Function Synthesis for Bit-Vector Relations. TACAS 2010: 236-250 - [c15]Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer:
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors. TACAS 2010: 280-295 - [c14]K. Rustan M. Leino, Philipp Rümmer:
A Polymorphic Intermediate Verification Language: Design and Logical Encoding. TACAS 2010: 312-327 - [i1]Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report). CoRR abs/1011.1036 (2010)
2000 – 2009
- 2009
- [c13]André Platzer, Jan-David Quesel, Philipp Rümmer:
Real World Verification. CADE 2009: 485-501 - [c12]Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher:
Mutation-Based Test Case Generation for Simulink Models. FMCO 2009: 208-227 - 2008
- [j1]Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter:
Integration of a security type system into a program logic. Theor. Comput. Sci. 402(2-3): 172-189 (2008) - [c11]Philipp Rümmer:
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. LPAR 2008: 274-289 - [c10]Helga Velroyen, Philipp Rümmer:
Non-termination Checking for Imperative Programs. TAP 2008: 154-170 - [c9]Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer:
Integrating Verification and Testing of Object-Oriented Software. TAP 2008: 182-191 - 2007
- [c8]Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
The KeY system 1.0 (Deduction Component). CADE 2007: 379-384 - [c7]Philipp Rümmer:
A Sequent Calculus for Integer Arithmetic with Counterexample Generation. VERIFY 2007 - [c6]Philipp Rümmer, Muhammad Ali Shah:
Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic. TAP 2007: 41-60 - [p1]Philipp Rümmer:
Construction of Proofs. The KeY Approach 2007: 179-242 - 2006
- [c5]Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt:
Verifying Object-Oriented Programs with KeY: A Tutorial. FMCO 2006: 70-101 - [c4]Philipp Rümmer:
Sequential, Parallel, and Quantified Updates of First-Order Structures. LPAR 2006: 422-436 - [c3]Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter:
Integration of a Security Type System into a Program Logic. TGC 2006: 116-131 - 2005
- [c2]Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
Verification of JCSP Programs. CPA 2005: 203-218 - 2004
- [c1]Richard Bubel, Andreas Roth, Philipp Rümmer:
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. LFM@IJCAR 2004: 107-128
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-02-08 00:51 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
