Publikationen
- Hojjat, Hossein, Konecn?, Filip, Garnier, Florent, Iosif, Radu, Kuncak, Viktor und Rümmer, Philipp (2012). A Verification Toolkit for Numerical Transition Systems - Tool Paper.
, 7436 in: Dimitra Giannakopoulou and Dominique Méry (eds.) FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. Springer, 247—251.
https://dx.doi.org/10.1007/978-3-642-32759-9_21 - Hojjat, Hossein, Iosif, Radu, Konecn?, Filip, Kuncak, Viktor und Rümmer, Philipp (2012). Accelerating Interpolants.
, 7561 in: Supratik Chakraborty and Madhavan Mukund (eds.) Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings. Springer, 187—202.
https://dx.doi.org/10.1007/978-3-642-33386-6_16 - Rümmer, Philipp (2012). Craig Interpolation for the Integers: Results, Implementation, and Experiences.
, 22 in: Konstantin Korovin and Stephan Schulz and Eugenia Ternovska (eds.) IWIL 2012: The 9th International Workshop on the Implementation of Logics, Merida, Venezuela, March 10, 2012. EasyChair, 3.
https://dx.doi.org/10.29007/9RXZ - Rümmer, Philipp (2012). E-Matching with Free Variables.
, 7180 in: Nikolaj S. Bj?rner and Andrei Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Springer, 359—374.
https://dx.doi.org/10.1007/978-3-642-28717-6_28 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp und Wahl, Thomas (2011). An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
J. Autom. Reason., 47 (4), 341—367.
https://dx.doi.org/10.1007/S10817-011-9237-Y - Donaldson, Alastair F., Kroening, Daniel und Rümmer, Philipp (2011). Automatic analysis of DMA races using model checking and \emphk-induction.
Formal Methods Syst. Des., 39 (1), 83—113.
https://dx.doi.org/10.1007/S10703-011-0124-2 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp und Wahl, Thomas (2011). Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.
, 6538 in: Ranjit Jhala and David A. Schmidt (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Springer, 88—102.
https://dx.doi.org/10.1007/978-3-642-18275-4_8 - Donaldson, Alastair F., Kroening, Daniel und Rümmer, Philipp (2011). SCRATCH: a tool for automatic analysis of dma races.
in: Calin Cascaval and Pen-Chung Yew (eds.) Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2011, San Antonio, TX, USA, February 12-16, 2011. ACM, 311—312.
https://dx.doi.org/10.1145/1941553.1941604 - Donaldson, Alastair F., Haller, Leopold, Kroening, Daniel und Rümmer, Philipp (2011). Software Verification Using k-Induction.
, 6887 in: Eran Yahav (eds.) Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. Springer, 351—368.
https://dx.doi.org/10.1007/978-3-642-23702-7_26 - He, Nannan, Rümmer, Philipp und Kroening, Daniel (2011). Test-case generation for embedded simulink via formal concept analysis.
in: Leon Stok and Nikil D. Dutt and Soha Hassoun (eds.) Proceedings of the 48th Design Automation Conference, DAC 2011, San Diego, California, USA, June 5-10, 2011. ACM, 224—229.
https://dx.doi.org/10.1145/2024724.2024777 - Leino, K. Rustan M. und Rümmer, Philipp (2010). A Polymorphic Intermediate Verification Language: Design and Logical Encoding.
, 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, 312—327.
https://dx.doi.org/10.1007/978-3-642-12002-2_26 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp und Wahl, Thomas (2010). An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
, 6173 in: Jürgen Giesl and Reiner H?hnle (eds.) Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. Springer, 384—399.
https://dx.doi.org/10.1007/978-3-642-14203-1_33 - Donaldson, Alastair F., Kroening, Daniel und Rümmer, Philipp (2010). Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.
, 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, 280—295.
https://dx.doi.org/10.1007/978-3-642-12002-2_24 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp und Wahl, Thomas (2010). Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report).
CoRR, abs/1011.1036 - Kroening, Daniel, Leroux, Jér?me und Rümmer, Philipp (2010). Interpolating Quantifier-Free Presburger Arithmetic.
, 6397 in: Christian G. Fermüller and Andrei Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings. Springer, 489—503.
https://dx.doi.org/10.1007/978-3-642-16242-8_35 - Ahrendt, Wolfgang, Beckert, Bernhard, Giese, Martin und Rümmer, Philipp (2010). Practical Aspects of Automated Deduction for Program Verification.
Künstliche Intell., 24 (1), 43—49.
https://dx.doi.org/10.1007/S13218-010-0001-Y - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp und 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 und 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 und 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 und 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 und 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 und 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 und 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 und 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