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). 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, 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 - 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 and Subotic, Pavle (2013). Exploring interpolants.
Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 69—76. - 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 - 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 - Rümmer, Philipp, Hojjat, Hossein and Kuncak, Viktor (2013). The Relationship between Craig Interpolation and Recursion-Free Horn Clauses.
CoRR, abs/1302.4187 - 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 - 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 - 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 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 - 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 - 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). 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 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 - 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 - 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 - 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). 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 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 - 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 - 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 - 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