Skip to main content


Publications in peer reviewed journals

  • Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and Wahl, Thomas (2010). Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays.
    , 3 in: Markus Aderhold and Serge Autexier and Heiko Mantel (eds.) 6th International Verification Workshop, VERIFY-2010, Edinburgh, UK, July 20-21, 2010. EasyChair, 31—46.
    https://dx.doi.org/10.29007/ZFKW
  • Cook, Byron, Kroening, Daniel, Rümmer, Philipp and Wintersteiger, Christoph M. (2010). Ranking Function Synthesis for Bit-Vector Relations.
    , 6015 in: Javier Esparza and Rupak Majumdar (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Springer, 236—250.
    https://dx.doi.org/10.1007/978-3-642-12002-2_19
  • Donaldson, Alastair F., He, Nannan, Kroening, Daniel and Rümmer, Philipp (2010). Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction.
    , 6957 in: Bernhard K. Aichernig and Frank S. de Boer and Marcello M. Bonsangue (eds.) Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers. Springer, 297—315.
    https://dx.doi.org/10.1007/978-3-642-25271-6_16
  • Brillout, Angelo, He, Nannan, Mazzucchi, Michele, Kroening, Daniel, Purandare, Mitra, Rümmer, Philipp and Weissenbacher, Georg (2009). Mutation-Based Test Case Generation for Simulink Models.
    , 6286 in: Frank S. de Boer and Marcello M. Bonsangue and Stefan Hallerstede and Michael Leuschel (eds.) Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers. Springer, 208—227.
    https://dx.doi.org/10.1007/978-3-642-17071-3_11
  • Platzer, André, Quesel, Jan-David and Rümmer, Philipp (2009). Real World Verification.
    , 5663 in: Renate A. Schmidt (eds.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Springer, 485—501.
    https://dx.doi.org/10.1007/978-3-642-02959-2_35
  • Rümmer, Philipp (2008). A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.
    , 5330 in: Iliano Cervesato and Helmut Veith and Andrei Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Springer, 274—289.
    https://dx.doi.org/10.1007/978-3-540-89439-1_20
  • Engel, Christian, Gladisch, Christoph, Klebanov, Vladimir and Rümmer, Philipp (2008). Integrating Verification and Testing of Object-Oriented Software.
    , 4966 in: Bernhard Beckert and Reiner Hähnle (eds.) Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. Springer, 182—191.
    https://dx.doi.org/10.1007/978-3-540-79124-9_13
  • Hähnle, Reiner, Pan, Jing, Rümmer, Philipp and Walter, Dennis (2008). Integration of a security type system into a program logic.
     Theor. Comput. Sci., 402 (2-3), 172—189.
    https://dx.doi.org/10.1016/J.TCS.2008.04.033
  • Velroyen, Helga and Rümmer, Philipp (2008). Non-termination Checking for Imperative Programs.
    , 4966 in: Bernhard Beckert and Reiner Hähnle (eds.) Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. Springer, 154—170.
    https://dx.doi.org/10.1007/978-3-540-79124-9_11
  • Rümmer, Philipp (2007). A Sequent Calculus for Integer Arithmetic with Counterexample Generation.
    , 259 in: Bernhard Beckert (eds.) Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007. CEUR-WS.org
  • Rümmer, Philipp (2007). Construction of Proofs.
    , 4334 in: Bernhard Beckert and Reiner Hähnle and Peter H. Schmitt (eds.) Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino. Springer, 179—242.
    https://dx.doi.org/10.1007/978-3-540-69061-0_4
  • Rümmer, Philipp and Shah, Muhammad Ali (2007). Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic.
    , 4454 in: Yuri Gurevich and Bertrand Meyer (eds.) Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers. Springer, 41—60.
    https://dx.doi.org/10.1007/978-3-540-73770-4_3
  • Beckert, Bernhard, Giese, Martin, Hähnle, Reiner, Klebanov, Vladimir, Rümmer, Philipp, Schlager, Steffen and Schmitt, Peter H. (2007). The KeY system 1.0 (Deduction Component).
    , 4603 in: Frank Pfenning (eds.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Springer, 379—384.
    https://dx.doi.org/10.1007/978-3-540-73595-3_26
  • Hähnle, Reiner, Pan, Jing, Rümmer, Philipp and Walter, Dennis (2006). Integration of a Security Type System into a Program Logic.
    , 4661 in: Ugo Montanari and Donald Sannella and Roberto Bruni (eds.) Trustworthy Global Computing, Second Symposium, TGC 2006, Lucca, Italy, November 7-9, 2006, Revised Selected Papers. Springer, 116—131.
    https://dx.doi.org/10.1007/978-3-540-75336-0_8
  • Rümmer, Philipp (2006). Sequential, Parallel, and Quantified Updates of First-Order Structures.
    , 4246 in: Miki Hermann and Andrei Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. Springer, 422—436.
    https://dx.doi.org/10.1007/11916277_29
  • Ahrendt, Wolfgang, Beckert, Bernhard, Hähnle, Reiner, Rümmer, Philipp and Schmitt, Peter H. (2006). Verifying Object-Oriented Programs with KeY: A Tutorial.
    , 4709 in: Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever (eds.) Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures. Springer, 70—101.
    https://dx.doi.org/10.1007/978-3-540-74792-5_4
  • Klebanov, Vladimir, Rümmer, Philipp, Schlager, Steffen and Schmitt, Peter H. (2005). Verification of JCSP Programs.
    , 63 in: Jan F. Broenink and Herman W. Roebbers and Johan P. E. Sunter and Peter H. Welch and David C. Wood (eds.) The 28th Communicating Process Architectures Conference, CPA 2005, organised under the auspices of WoTUG, Philips and the Technische Universiteit Eindhoven, Eindhoven, The Netherlands, 18-21 September 2005. IOS Press, 203—218.
  • Bubel, Richard, Roth, Andreas and Rümmer, Philipp (2004). Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic.
    , 199 in: Carsten Schürmann (eds.) Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, LFM@IJCAR 2004. Cork, Ireland, July 5, 2004. Elsevier, 107—128.
    https://dx.doi.org/10.1016/J.ENTCS.2007.11.015
To top