Publications in peer reviewed journals
- Arlt, Stephan, Rümmer, Philipp and Schäf, Martin (2013) A Theory for Control-Flow Graph Exploration.
, 8172 in: Dang Van Hung and Mizuhito Ogawa (eds.) Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings. Springer, 506—515.
https://dx.doi.org/10.1007/978-3-319-02444-8_44 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) The Relationship between Craig Interpolation and Recursion-Free Horn Clauses.
CoRR, abs/1302.4187 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report).
CoRR, abs/1301.4973 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Classifying and Solving Horn Clauses for Verification.
, 8164 in: Ernie Cohen and Andrey Rybalchenko (eds.) Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers. Springer, 1—21.
https://dx.doi.org/10.1007/978-3-642-54108-7_1 - Rümmer, Philipp and Subotic, Pavle (2013) Exploring interpolants.
Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 69—76. - Cook, Byron, Kroening, Daniel, Rümmer, Philipp and Wintersteiger, Christoph M. (2013) Ranking function synthesis for bit-vector relations.
Formal Methods Syst. Des., 43 (1), 93—120.
https://dx.doi.org/10.1007/S10703-013-0186-4 - Arlt, Stephan, Rümmer, Philipp and Schäf, Martin (2013) Joogie: from Java through Jimple to Boogie.
in: Patrick Lam and Elena Sherman (eds.) Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysis, SOAP 2013, Seattle, WA, USA, June 20, 2013. ACM, 3—8.
https://dx.doi.org/10.1145/2487568.2487570 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013) Disjunctive Interpolants for Horn-Clause Verification.
, 8044 in: Natasha Sharygina and Helmut Veith (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Springer, 347—363.
https://dx.doi.org/10.1007/978-3-642-39799-8_24 - Hojjat, Hossein, Konecný, Filip, Garnier, Florent, Iosif, Radu, Kuncak, Viktor and 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 - 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 - Hojjat, Hossein, Iosif, Radu, Konecný, Filip, Kuncak, Viktor and 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 - He, Nannan, Rümmer, Philipp and 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 - Donaldson, Alastair F., Haller, Leopold, Kroening, Daniel and 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 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and 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 and 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 - Donaldson, Alastair F., Kroening, Daniel and 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 - Brillout, Angelo, Kroening, Daniel, Rümmer, Philipp and 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 - Daim, Tugrul U., Lim, Donggyu, Gomez, Fredy A., Schwarz, Justus and Jovanovic, Stevan (2014). Storage technologies for wind power in the Columbia River Gorge.
International Journal of Sustainable Energy, 33 (1) Taylor & Francis, 1-15.
https://dx.doi.org/10.1080/14786451.2011.630467 - Kroening, Daniel, Leroux, Jérôme and 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 - 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., Kroening, Daniel and 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 - Leino, K. Rustan M. and 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 and Wahl, Thomas (2010) Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report).
CoRR, abs/1011.1036 - Ahrendt, Wolfgang, Beckert, Bernhard, Giese, Martin and 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