Peer-Reviewed Articles

Also see DBLP and Google Scholar.

2022

  1. 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
    Proceedings of the ACM on Programming Languages (POPL), Volume 6 Issue POPL, January 2022
    (PDF - BibTeX - Abstract)
  2. Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader
    CertiStr: a certified string solver
    11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA
    Distinguished-paper award
    (PDF - BibTeX - Abstract)
  3. Wolfgang Ahrendt, Dilian Gurov, Moa Johansson, Philipp Rümmer
    TriCo - Triple Co-piloting of Implementation, Specification and Tests
    11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). Rhodes, Greece, 2022
    Springer-Verlag, LNCS 13701, pages 174-187
    (PDF - BibTeX - Abstract)
  4. Chencheng Liang, Philipp Rümmer, Marc Brockschmidt
    Exploring Representation of Horn clauses using GNNs
    Workshop on Practical Aspects of Automated Reasoning (PAAR) at FLoC, Haifa, Israel, 2022
    (PDF - BibTeX - Abstract)
  5. Zafer Esen, Philipp Rümmer
    An SMT-LIB Theory of Heaps
    20th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, Haifa, Israel, 2022
    (PDF - BibTeX - Abstract)

2021

  1. Peter Backeman, Philipp Rümmer, Aleksandar Zeljic
    Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
    Formal Methods in System Design 57(2): 121-156 (2021)
    (PDF Preprint - BibTeX - Abstract)
  2. Ali Shamakhi, Hossein Hojjat, Philipp Rümmer
    Towards String Support in JayHorn (Competition Contribution)
    27th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Held as part of ETAPS
    Springer-Verlag, LNCS 12652, pages 443-447
    (PDF Preprint - BibTeX - Abstract - Implementation)

2020

  1. Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
    A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
    18th International Symposium on Automated Technology for Verification and Analysis (ATVA), Hanoi, Vietnam
    Springer, LNCS 12302, pages 325-342
    (PDF Preprint - BibTeX - Abstract)
  2. Zafer Esen, Philipp Rümmer
    Towards an SMT-LIB Theory of Heap
    Extended abstract at the 7th Workshop on Horn Clauses for Verification and Synthesis (HCVS)
    EPTCS, volume 320, pages 159-162
    (PDF - BibTeX)
  3. Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
    Monadic Decomposition in Integer Linear Arithmetic
    10th International Joint Conference on Automated Reasoning (IJCAR), 2020, Paris, France
    Springer, LNCS 12166, pages 122-140
    (PDF Preprint - BibTeX - Abstract)

2019

  1. Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer
    Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols)
    Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA
    Springer, LNCS 11561, pages 455-474
    (PDF Preprint - BibTeX - Abstract)
  2. Temesghen Kahsai, Philipp Rümmer, Martin Schäf
    JayHorn: A Java Model Checker (Competition Contribution)
    Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019
    Springer-Verlag, LNCS 11429, pages 214-218
    (PDF Preprint - BibTeX - Abstract - Implementation)
  3. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
    Decision procedures for path feasibility of string-manipulating programs with complex operations
    Symposium on Principles of Programming Languages (POPL), Cascais, Portugal
    Proceedings of the ACM on Programming Languages, Volume 3 Issue POPL, January 2019, pages 49:1-49:30
    (PDF Preprint - BibTeX - Abstract - Implementation)

2018

  1. Peter Backeman, Philipp Rümmer, Aleksandar Zeljic
    Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
    Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA
    IEEE
    (PDF Preprint - BibTeX - Abstract)
  2. Hossein Hojjat, Philipp Rümmer
    The Eldarica Horn Solver
    Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA
    IEEE
    (PDF Preprint - BibTeX - Abstract)
  3. 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
    Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA
    IEEE
    (PDF Preprint - BibTeX - Abstract - Implementation)
  4. Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer
    Exploring Approximations for Floating-Point Arithmetic Using UppSAT
    9th International Joint Conference on Automated Reasoning (IJCAR), 2018, Oxford, UK
    Springer, LNCS 10900, pages 246-262
    (PDF Preprint - BibTeX - Abstract - Implementation)
  5. Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
    Automating regression verification of pointer programs by predicate abstraction
    Formal Methods in System Design 52(3): 229-259 (2018)
    (PDF Preprint - BibTeX - Abstract)
  6. Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar
    String constraints with concatenation and transducers solved efficiently
    Symposium on Principles of Programming Languages (POPL), Los Angeles, USA
    Proceedings of the ACM on Programming Languages, Volume 2 Issue POPL, January 2018, pages 4:1-4:32
    (PDF Preprint - BibTeX - Abstract - Implementation)

2017

  1. Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer
    Learning to Prove Safety over Parameterised Concurrent Systems
    IEEE, Formal Methods in Computer-Aided Design (FMCAD), 2017, Vienna, Austria
    IEEE, pages 76--83
    (PDF Preprint - BibTeX - Abstract - Extended technical report)
  2. Hossein Hojjat, Philipp Rümmer
    Deciding and Interpolating Algebraic Data Types by Reduction
    19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), Timisoara, Romania
    IEEE Computer Society, pages 145--152
    (Extended PDF Preprint - BibTeX - Abstract)
  3. Nikolaj Bjørner, Dejan Jovanovic, Tancrčde Lepoint, Philipp Rümmer, Martin Schäf
    Abduction by Non-Experts
    IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana
    (PDF Preprint - BibTeX - Abstract)
  4. Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Martin Schäf
    Quantified Heap Invariants for Object-Oriented Programs
    Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana
    EPiC Series in Computing, volume 46, pages 368-384
    (PDF Preprint - BibTeX - Abstract - Implementation)
  5. Yulia Demyanova, Philipp Rümmer, Florian Zuleger
    Systematic Predicate Abstraction Using Variable Roles
    9th NASA Formal Methods Symposium (NFM), 2017, Moffett Field, CA, USA
    Springer, LNCS 10227, pages 265-281
    (PDF Preprint - BibTeX - Abstract)
  6. 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
    Programming Language Design and Implementation (PLDI), 2017, Barcelona, Spain
    ACM, pages 602-617
    (PDF Preprint - BibTeX - Abstract)
  7. Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rümmer
    Fair Termination for Parameterized Probabilistic Concurrent Systems
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Uppsala, Sweden, April 2017
    Springer, LNCS 10205, pages 499-517
    (PDF Preprint - BibTeX - Abstract)
  8. Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
    An Approximation Framework for Solvers and Decision Procedures
    Journal of Automated Reasoning, Volume 58 / 2017, Issue 1, Pages 127-147
    (PDF Preprint - DOI - BibTeX - Abstract)

2016

  1. Hossein Hojjat, Philipp Rümmer, Jedidiah McClurg, Pavol Cerny, Nate Foster
    Optimizing Horn Solvers for Network Repair
    IEEE, Formal Methods in Computer-Aided Design (FMCAD), 2016, Mountain View, USA
    (PDF Preprint - BibTeX - Abstract)
  2. Anthony W. Lin, Philipp Rümmer
    Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
    28th International Conference on Computer Aided Verification, Toronto, Canada
    Springer, LNCS 9780, pages 112-133
    (PDF Preprint - BibTeX - Abstract - Implementation - Extended technical report)
  3. Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez, Martin Schäf
    JayHorn: A Framework for Verifying Java programs
    28th International Conference on Computer Aided Verification, Toronto, Canada
    Springer, LNCS 9779, pages 352-358
    (PDF Preprint - BibTeX - Abstract - Implementation)
  4. Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
    Deciding Bit-Vector Formulas with mcSAT
    19th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2016, Bordeaux, France
    Springer, LNCS 9710, pages 249-266
    (PDF Preprint - BibTeX - Abstract - Implementation)
  5. Anthony W. Lin, Truong Khanh Nguyen, Philipp Rümmer, Jun Sun
    Regular Symmetry Patterns
    17th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2016, St. Petersburg, Florida
    Springer, LNCS 9583, pages 455-475
    (PDF Preprint - BibTeX - Abstract - Implementation - Extended technical report)
  6. Jérôme Leroux, Philipp Rümmer, Pavle Subotic
    Guiding Craig Interpolation with Domain-specific Abstractions
    Acta Informatica 53(4): 387-424, 2016
    (PDF Preprint - BibTeX - Abstract - Implementation)

2015

  1. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
    On recursion-free Horn clauses and Craig interpolation
    Formal Methods in System Design 47(1): 1-25 (2015)
    (PDF Preprint - BibTeX - Abstract)
  2. Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
    An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
    22. IEEE Symposium on Computer Arithmetic 2015, Lyon, France
    IEEE 2015, pages 160-167
    (PDF of extended report - BibTeX - Abstract)
  3. 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
    27th International Conference on Computer Aided Verification (CAV), 2015, San Francisco, CA, USA
    Springer, LNCS 9206, pages 462-469
    (PDF Preprint - BibTeX - Abstract - Implementation)
  4. Peter Backeman, Philipp Rümmer
    Efficient Algorithms for Bounded Rigid E-unification
    Automated Reasoning with Analytic Tableaux and Related Methods, 24th International Conference, TABLEAUX 2015
    Springer, LNCS 9323, pages 70-85
    (PDF Preprint - BibTeX - Abstract - Implementation)
  5. Peter Backeman, Philipp Rümmer
    Theorem Proving with Bounded Rigid E-Unification
    25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015
    Springer, LNCS 9195, pages 572-587
    (PDF Preprint - BibTeX - Abstract - Implementation)
  6. Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanovic, Philipp Rümmer, Thomas Wies
    Conflict-Directed Graph Coverage
    Seventh NASA Formal Methods Symposium (NFM), 2015, Pasadena, CA, USA
    Springer, LNCS 9058, pages 327-342
    (PDF Preprint - BibTeX - Abstract)
  7. Daniel Schwartz-Narbonne, Philipp Rümmer, Martin Schäf, Ashish Tiwari, Thomas Wies
    Non-Monotonic Program Analysis
    Workshop on Horn Clauses for Verification and Synthesis (HCVS), 2015, San Francisco, USA
    (PDF Preprint - BibTeX - Abstract)
  8. Tim McCarthy, Philipp Rümmer, Martin Schäf
    Bixie: Finding and Understanding Inconsistent Code
    37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy
    Volume 2. IEEE 2015, pages 645-648
    (PDF Preprint - BibTeX - Abstract - Implementation)
  9. Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
    Automating regression verification
    Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März - 20. März 2015, Dresden, Germany
    Lecture Notes in Informatics 239, pages 75-76
    (PDF Preprint - BibTeX - Abstract - Webpage)

2014

  1. Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich
    Automating regression verification
    29th IEEE/ACM International Conference on Automated Software Engineering (ASE), Västerås, Sweden
    ACM New York, NY, USA, 978-1-4503-3013-8, pages 349-360
    (PDF Preprint - BibTeX - Abstract - Webpage)
  2. Hossein Hojjat, Philipp Rümmer, Pavle Subotic, Wang Yi
    Horn Clauses for Communicating Timed Systems
    Workshop on Horn Clauses for Verification and Synthesis (HCVS), 2014, Vienna, Austria
    Electronic Proceedings in Theoretical Computer Science (EPTCS), 169
    (PDF - Bibtex - Abstract)
  3. Stephan Arlt, John Murray, Philipp Rümmer, Martin Schäf
    Quantification of Verification Progress
    Second VeriSure Workshop, 2014, Vienna, Austria
    (PDF - Bibtex - Abstract)
  4. Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer
    Approximations for Model Construction
    7th International Joint Conference on Automated Reasoning (IJCAR), 2014, Vienna, Austria
    Springer, LNCS 8562, pages 344-359
    Best-paper award
    (PDF Preprint - BibTeX - Abstract - Implementation)
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
    String Constraints for Verification
    26th International Conference on Computer Aided Verification (CAV), 2014, Vienna, Austria
    Springer, LNCS 8559, pages 150-166
    (PDF Preprint - BibTeX - Abstract - Implementation)
    Note: reference [9] in the paper is incorrect, and should actually point to this article. We apologise for the mistake.
  6. Stephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf, Natarajan Shankar
    The Gradual Verifier
    Sixth NASA Formal Methods Symposium (NFM), 2014, Houston, USA
    Springer, LNCS 8430, pages 313-327
    (PDF Preprint - BibTeX - Abstract)

2013

  1. Philipp Rümmer, Pavle Subotic
    Exploring Interpolants
    IEEE, Formal Methods in Computer-Aided Design (FMCAD), 2013, Portland, USA
    (PDF Preprint - BibTeX - Abstract)
  2. Stephan Arlt, Philipp Rümmer, Martin Schäf
    A Theory for Control-Flow Graph Exploration
    11th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2013, Hanoi, Vietnam
    Springer, LNCS 8172, pages 506-515
    (PDF Preprint - BibTeX - Abstract)
  3. Stephan Arlt, Philipp Rümmer, Martin Schäf
    Joogie: From Java through Jimple to Boogie
    ACM SIGPLAN International Workshop on the State Of the Art in Java Program Analysis (SOAP), 2013, Seattle, USA
    (PDF Preprint - BibTeX - Abstract)
  4. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
    Classifying and Solving Horn Clauses for Verification
    Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), 2013, Atherton, USA
    Springer, LNCS 8164, pages 1-21
    (PDF Preprint - BibTeX - Abstract)
  5. Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
    Disjunctive Interpolants for Horn-Clause Verification
    25th International Conference on Computer Aided Verification (CAV), 2013, St. Petersburg, Russia
    Springer, LNCS 8044, pages 347-363
    (PDF Preprint - BibTeX - Abstract)
  6. Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
    Ranking Function Synthesis for Bit-Vector Relations
    Formal Methods in System Design 43(1): 93-120 (2013)
    (PDF Preprint - BibTeX - Abstract - More information - Seneschal)

2012

  1. Hossein Hojjat, Radu Iosif, Filip Konecny, Viktor Kuncak, Philipp Rümmer
    Accelerating Interpolants
    Automated Technology for Verification and Analysis (ATVA), 2012, Thiruvananthapuram, Kerala, India
    Springer, LNCS 7561, pages 187-202
    (PDF Preprint - BibTeX - Abstract)
  2. Hossein Hojjat, Filip Konecny, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer
    A Verification Toolkit for Numerical Transition Systems
     16th International Symposium on Formal Methods (FM), 2012, Paris, France
    Springer, LNCS 7436, pages 247-251
    (PDF Preprint - BibTeX - Abstract)
  3. Philipp Rümmer
    E-Matching with Free Variables
    18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mérida, Venezuela, March 2012
    Springer, LNCS 7180, pages 359-374
    (PDF Preprint - BibTeX - Abstract)
  4. Nannan He, Daniel Kroening, Thomas Wahl, Kung-Kiu Lau, Faris Taweel, Cuong M. Tran, Philipp Rümmer, Sanjiv S. Sharma
    Component-based Design and Verification in X-MAN
    ERTS2 2012: Embedded Real Time Software and Systems, 2012, Toulouse, France
    (PDF - BibTeX - Abstract)
  5. Alastair F. Donaldson, Nannan He, Philipp Rümmer, Daniel Kroening
    Tightening test coverage metrics: A case study in equivalence checking using k-induction
    9th International Symposium on Formal Methods for Components and Objects (FMCO), 2010, Graz, Austria. Revised Papers
    Springer, LNCS 6957, pages 297-315
    (PDF Preprint - BibTeX - Abstract)

2011

  1. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
    An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    Journal of Automated Reasoning, Volume 47 / 2011, Issue 4, Pages 341-367
    Special Issue on Selected Papers from the 5th International Joint Conference on Automated Reasoning (IJCAR)
    (PDF Preprint - DOI - BibTeX - Abstract)
  2. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
    Automatic Analysis of DMA Races Using Model Checking and k-induction
    International Journal on Formal Methods in System Design (FMSD), Volume 39 / 2011, Number 1, pages 83-113
    (PDF Preprint - DOI - BibTeX - Abstract)
  3. Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer
    Software Verification Using k-Induction
    18th International Static Analysis Symposium (SAS), Venice, Italy, September 2011
    Springer, LNCS 6887, pages 351-368
    (PDF Preprint - BibTeX - Abstract - Implementation)
  4. Nannan He, Philipp Rümmer, Daniel Kroening
    Test-case generation for embedded Simulink via formal concept analysis
    Design Automation Conference (DAC), San Diego, USA, June 2011
    Nominated for best-paper award
    (PDF Preprint - BibTeX - Abstract)
  5. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
    SCRATCH: a tool for automatic analysis of DMA races
    Poster at 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP), San Antonio, TX, USA, 2011
    (PDF - BibTeX - Abstract - Implementation)
  6. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
    Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
    12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Austin, Texas, January 2011
    Springer, LNCS 6538, pages 88-102
    (PDF Preprint - BibTeX - Abstract - Implementation)

2010

  1. Daniel Kroening, Jérôme Leroux, Philipp Rümmer
    Interpolating Quantifier-Free Presburger Arithmetic
    17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Yogyakarta, Indonesia, October 2010
    Springer, LNCS 6397, pages 489-503
    (PDF Preprint - BibTeX - Abstract)
  2. Philipp Rümmer, Thomas Wahl
    An SMT-LIB Theory of Binary Floating-Point Arithmetic
    8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, Edinburgh, Scotland, July 2010
    (PDF - BibTeX - Abstract)
  3. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
    Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
    6th International Verification Workshop (VERIFY) at FLoC, Edinburgh, Scotland, July 2010
    (PDF - BibTeX - Abstract - Implementation)
  4. Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl
    An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
    International Joint Conference on Automated Reasoning (IJCAR) at FLoC, Edinburgh, Scotland, July 2010
    Springer, LNCS 6173, pages 384-399
    (PDF Preprint - BibTeX - Abstract)
  5. Angelo Brillout, Nannan He, Michele Mazzucchi, Daniel Kroening, Mitra Purandare, Philipp Rümmer, Georg Weissenbacher
    Mutation-based Test Case Generation for Simulink Models
    International Symposium on Formal Methods for Components and Objects, Eindhoven, The Netherlands, November 2009
    Springer, LNCS 6286, pages 208-227
    (PDF Preprint - BibTeX - Abstract)
  6. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
    Analysing DMA Races in Multicore Software
    3rd Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES'10) at ETAPS 2010
    (PDF - BibTeX - Abstract)
  7. Alastair F. Donaldson, Daniel Kroening, Philipp Rümmer
    Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
    16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
    Springer, LNCS 6015, pages 280-295
    (PDF Preprint - BibTeX - Abstract - Implementation)
  8. Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger
    Ranking Function Synthesis for Bit-Vector Relations
    16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
    Springer, LNCS 6015, pages 236-250
    (PDF Preprint - BibTeX - Abstract - More information - Seneschal)
  9. K. Rustan M. Leino, Philipp Rümmer
    A Polymorphic Intermediate Verification Language: Design and Logical Encoding
    16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, Cyprus, March 2010
    Springer, LNCS 6015, pages 312-327
    (PDF Preprint - BibTeX - Abstract)

2009

  1. Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer
    Practical Aspects of Automated Deduction for Program Verification
    KI Journal, Volume 24 / 2010, Number 1, pages 43-49
    (PDF Preprint - BibTeX - Abstract)
  2. Daniel Kröning, Philipp Rümmer, Georg Weissenbacher
    A Proposal for a Theory of Finite Sets, Lists, and Maps for the SMT-Lib Standard
    7th International Workshop on Satisfiability Modulo Theories at CADE, Montreal, Canada, August 2009
    In informal workshop proceedings
    (PDF - BibTeX - Abstract)
  3. André Platzer, Jan-David Quesel, Philipp Rümmer
    Real World Verification
    22nd International Conference on Automated Deduction (CADE), Montreal, Canada, August 2009
    Springer, LNCS 5663, pages 485-501
    (PDF Preprint - BibTeX - Abstract - More information)

2008

  1. Philipp Rümmer
    A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
     15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Doha, Qatar, 2008
    Springer, LNCS 5330, pages 274-289
    (PDF Preprint - BibTeX - Abstract - Implementation)
    My PhD thesis contains an extended version of the paper.
  2. Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
    Integration of a Security Type System into a Program Logic
    Theoretical Computer Science, Volume 402, Issues 2-3, 8 August 2008, pages 172-189
    (Special Issue with selected papers from TGC 2006)
    (PDF Preprint - BibTeX - Abstract)
  3. Helga Velroyen, Philipp Rümmer
    Non-Termination Checking for Imperative Programs
     2nd International Conference on Tests and Proofs, Prato, Italy, 2008
    Springer, LNCS 4966, pages 154-170
    (PDF Preprint - BibTeX - Abstract - Implementation)
  4. Richard Bubel, Andreas Roth, and Philipp Rümmer
    Ensuring Correctness of Lightweight Tactics for Java Card Dynamic Logic
    Workshop on Logical Frameworks and Meta-Languages (LFM) at IJCAR 2004, 2004
    ENTCS Volume 199, 24 February 2008, Pages 107-128
    (PDF Preprint - DOI - BibTeX - Abstract)

2007

  1. Philipp Rümmer
    A Sequent Calculus for Integer Arithmetic with Counterexample Generation
     4th International Verification Workshop at CADE 21, Bremen, Germany, July 2007
    CEUR Workshop Proceedings, Vol 259
    (PDF - BibTeX - Abstract)
  2. Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt
    The KeY System (Deduction Component)
    System abstract, International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007
    Springer, LNCS 4603, pages 379-384
    (PDF Preprint - BibTeX - Abstract)
  3. Philipp Rümmer, Muhammad Ali Shah
    Proving Programs Incorrect using a Sequent Calculus for Java Dynamic Logic
    International Conference on Tests And Proofs (TAP), ETH Zürich, Switzerland, Februrary 2007
    Springer, LNCS 4454, pages 41-60
    (PDF Preprint - BibTeX - Abstract)

2006

  1. Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt
    Verifying Object-Oriented Programs with KeY: A Tutorial
     5th International Symposium on Formal Methods for Components and Objects, Amsterdam, The Netherlands, November 2006
    Springer, LNCS 4709, pages 70-101
    (PDF Preprint - BibTeX - Abstract - Example of the paper - Talk)
  2. Reiner Hähnle, Jing Pan, Philipp Rümmer, Dennis Walter
    Integration of a Security Type System into a Program Logic
    2nd Symposium on Trustworthy Global Computing (TGC), Lucca, Italy, November 2006
    Springer, LNCS 4661, pages 116-131
    (PDF Preprint - BibTeX - Abstract)
  3. Philipp Rümmer
    Sequential, Parallel, and Quantified Updates of First-Order Structures
    13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Phnom Penh, Cambodia, November 2006
    Springer, LNCS 4246, pages 422-436
    (PDF (preprint) - BibTeX - Abstract)
    My PhD thesis contains an extended version of the paper.
    There is also a formalisation of theorems given in the paper in Isabelle/HOL

2005

  1. Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
    Verification of JCSP Programs
     Communicating Process Architectures, Eindhoven, The Netherlands, September 2005
    IOS Press, volume 63 of Concurrent Systems Engineering Series, pages 203-218, The Netherlands
    (PDF - BibTeX - Abstract)
  2. Philipp Rümmer
    Generating Counterexamples for Java Dynamic Logic
    Informal Proceedings of Workshop on Disproving at CADE 20, 2005
    (Postscript - BibTeX - Abstract)