×
Compute Distance To:
Author ID: rummer.philipp Recent zbMATH articles by "Rümmer, Philipp"
Published as: Rümmer, Philipp; Rümmer, Phillipp

Publications by Year

Citations contained in zbMATH Open

33 Publications have been cited 146 times in 104 Documents Cited by Year
A constraint sequent calculus for first-order logic with linear integer arithmetic. Zbl 1182.03035
Rümmer, Philipp
20
2008
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
13
2010
Ranking function synthesis for bit-vector relations. Zbl 1284.68172
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
11
2010
Sequential, parallel, and quantified updates of first-order structures. Zbl 1165.68376
Rümmer, Philipp
10
2006
Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
10
2011
Real world verification. Zbl 1250.68197
Platzer, André; Quesel, Jan-David; Rümmer, Philipp
7
2009
Non-termination checking for imperative programs. Zbl 1138.68460
Velroyen, Helga; Rümmer, Philipp
7
2008
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
7
2011
A polymorphic intermediate verification language: design and logical encoding. Zbl 1284.68409
Leino, K. Rustan M.; Rümmer, Philipp
6
2010
Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148
Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp
5
2010
Theorem proving with bounded rigid \(E\)-unification. Zbl 1431.03022
Backeman, Peter; Rümmer, Philipp
4
2015
Deciding bit-vector formulas with mcSAT. Zbl 1475.68226
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
4
2016
E-matching with free variables. Zbl 1352.68214
Rümmer, Philipp
4
2012
Ranking function synthesis for bit-vector relations. Zbl 1291.68138
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
4
2013
On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134
Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor
3
2015
Efficient algorithms for bounded rigid \(E\)-unification. Zbl 1471.68300
Backeman, Peter; Rümmer, Philipp
3
2015
Guiding Craig interpolation with domain-specific abstractions. Zbl 1344.68139
Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle
3
2016
Proving programs incorrect using a sequent calculus for Java dynamic logic. Zbl 1196.68053
Rümmer, Philipp; Shah, Muhammad Ali
3
2007
Integration of a security type system into a program logic. Zbl 1211.68089
Hähnle, Reiner; Pan, Jing; Rümmer, Philipp; Walter, Dennis
3
2007
Accelerating interpolants. Zbl 1374.68291
Hojjat, Hossein; Iosif, Radu; Konečný, Filip; Kuncak, Viktor; Rümmer, Philipp
3
2012
Quantified heap invariants for object-oriented programs. Zbl 1403.68126
Kahsai, Temesghen; Kersten, Rody; Rümmer, Philipp; Schäf, Martin
2
2017
Liveness of randomised parameterised systems under arbitrary schedulers. Zbl 1411.68075
Lin, Anthony W.; Rümmer, Philipp
2
2016
Fair termination for parameterized probabilistic concurrent systems. Zbl 1452.68127
Lengál, Ondřej; Lin, Anthony W.; Majumdar, Rupak; Rümmer, Philipp
2
2017
Approximations for model construction. Zbl 1409.68264
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2014
Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124
Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp
1
2011
Taclets: a new paradigm for constructing interactive theorem provers. Zbl 1103.68798
Beckert, Bernhard; Giese, Martin; Habermalz, Elmar; Hähnle, Reiner; Roth, Andreas; Rümmer, Phillipp; Schlager, Steffen
1
2004
Verified software. Theories, tools, and experiments. 10th international conference, VSTTE 2018, Oxford, UK, July 18–19, 2018. Revised selected papers. Zbl 1400.68034
1
2018
Exploring approximations for floating-point arithmetic using uppsat. Zbl 06958103
Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2018
Integration of a security type system into a program logic. Zbl 1146.68029
Hähnle, Reiner; Pan, Jing; Rümmer, Philipp; Walter, Dennis
1
2008
An approximation framework for solvers and decision procedures. Zbl 1409.68265
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2017
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic. Zbl 1278.68251
Bubel, Richard; Roth, Andreas; Rümmer, Philipp
1
2007
Horn clauses for communicating timed systems. Zbl 1464.68207
Hojjat, Hossein; Rümmer, Philipp; Subotic, Pavle; Yi, Wang
1
2014
Towards an SMT-LIB theory of heap. Zbl 07453198
Esen, Zafer; Rümmer, Philipp
1
2020
Towards an SMT-LIB theory of heap. Zbl 07453198
Esen, Zafer; Rümmer, Philipp
1
2020
Verified software. Theories, tools, and experiments. 10th international conference, VSTTE 2018, Oxford, UK, July 18–19, 2018. Revised selected papers. Zbl 1400.68034
1
2018
Exploring approximations for floating-point arithmetic using uppsat. Zbl 06958103
Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2018
Quantified heap invariants for object-oriented programs. Zbl 1403.68126
Kahsai, Temesghen; Kersten, Rody; Rümmer, Philipp; Schäf, Martin
2
2017
Fair termination for parameterized probabilistic concurrent systems. Zbl 1452.68127
Lengál, Ondřej; Lin, Anthony W.; Majumdar, Rupak; Rümmer, Philipp
2
2017
An approximation framework for solvers and decision procedures. Zbl 1409.68265
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2017
Deciding bit-vector formulas with mcSAT. Zbl 1475.68226
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
4
2016
Guiding Craig interpolation with domain-specific abstractions. Zbl 1344.68139
Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle
3
2016
Liveness of randomised parameterised systems under arbitrary schedulers. Zbl 1411.68075
Lin, Anthony W.; Rümmer, Philipp
2
2016
Theorem proving with bounded rigid \(E\)-unification. Zbl 1431.03022
Backeman, Peter; Rümmer, Philipp
4
2015
On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134
Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor
3
2015
Efficient algorithms for bounded rigid \(E\)-unification. Zbl 1471.68300
Backeman, Peter; Rümmer, Philipp
3
2015
Approximations for model construction. Zbl 1409.68264
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp
1
2014
Horn clauses for communicating timed systems. Zbl 1464.68207
Hojjat, Hossein; Rümmer, Philipp; Subotic, Pavle; Yi, Wang
1
2014
Ranking function synthesis for bit-vector relations. Zbl 1291.68138
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
4
2013
E-matching with free variables. Zbl 1352.68214
Rümmer, Philipp
4
2012
Accelerating interpolants. Zbl 1374.68291
Hojjat, Hossein; Iosif, Radu; Konečný, Filip; Kuncak, Viktor; Rümmer, Philipp
3
2012
Beyond quantifier-free interpolation in extensions of Presburger arithmetic. Zbl 1318.03045
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
10
2011
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1259.03043
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
7
2011
Automatic analysis of DMA races using model checking and \(k\)-induction. Zbl 1233.68124
Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp
1
2011
An interpolating sequent calculus for quantifier-free Presburger arithmetic. Zbl 1291.03112
Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas
13
2010
Ranking function synthesis for bit-vector relations. Zbl 1284.68172
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
11
2010
A polymorphic intermediate verification language: design and logical encoding. Zbl 1284.68409
Leino, K. Rustan M.; Rümmer, Philipp
6
2010
Interpolating quantifier-free Presburger arithmetic. Zbl 1306.68148
Kroening, Daniel; Leroux, Jérôme; Rümmer, Philipp
5
2010
Real world verification. Zbl 1250.68197
Platzer, André; Quesel, Jan-David; Rümmer, Philipp
7
2009
A constraint sequent calculus for first-order logic with linear integer arithmetic. Zbl 1182.03035
Rümmer, Philipp
20
2008
Non-termination checking for imperative programs. Zbl 1138.68460
Velroyen, Helga; Rümmer, Philipp
7
2008
Integration of a security type system into a program logic. Zbl 1146.68029
Hähnle, Reiner; Pan, Jing; Rümmer, Philipp; Walter, Dennis
1
2008
Proving programs incorrect using a sequent calculus for Java dynamic logic. Zbl 1196.68053
Rümmer, Philipp; Shah, Muhammad Ali
3
2007
Integration of a security type system into a program logic. Zbl 1211.68089
Hähnle, Reiner; Pan, Jing; Rümmer, Philipp; Walter, Dennis
3
2007
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic. Zbl 1278.68251
Bubel, Richard; Roth, Andreas; Rümmer, Philipp
1
2007
Sequential, parallel, and quantified updates of first-order structures. Zbl 1165.68376
Rümmer, Philipp
10
2006
Taclets: a new paradigm for constructing interactive theorem provers. Zbl 1103.68798
Beckert, Bernhard; Giese, Martin; Habermalz, Elmar; Hähnle, Reiner; Roth, Andreas; Rümmer, Phillipp; Schlager, Steffen
1
2004
all top 5

Cited by 218 Authors

17 Rümmer, Philipp
12 Kröning, Daniel
7 Hähnle, Reiner
4 Backeman, Peter
4 Biere, Armin
4 Bonacina, Maria Paola
4 Bubel, Richard
4 Griggio, Alberto
4 Weiss, Benjamin
4 Wintersteiger, Christoph M.
3 Ábrahám, Erika
3 Bjørner, Nikolaj S.
3 Brillout, Angelo
3 Bruttomesso, Roberto
3 Davenport, James Harold
3 England, Matthew
3 Fontaine, Pascal
3 Ghilardi, Silvio
3 Graham-Lengrand, Stéphane
3 Ranise, Silvio
3 Sebastiani, Roberto
3 Sharygina, Natasha
3 Ulbrich, Mattias
3 Wahl, Thomas
2 Abbott, John A.
2 Baumgartner, Peter
2 Becker, Bernd
2 Bigatti, Anna Maria
2 Blanchette, Jasmin Christian
2 Böhme, Sascha
2 Brain, Martin
2 Buchberger, Bruno
2 Bury, Guillaume
2 Cimatti, Alessandro
2 de Moura, Leonardo
2 Delahaye, David
2 Forrest, Stephen
2 Frohn, Florian
2 Giesl, Jürgen
2 Gladisch, Christoph D.
2 Hensel, Jera
2 Johansson, Moa
2 Kuncak, Viktor
2 McMillan, Kenneth L.
2 Niemetz, Aina
2 Paskevich, Andrei
2 Paulson, Lawrence Charles
2 Preiner, Mathias
2 Reynolds, Andrew
2 Rybalchenko, Andrey
2 Schmitt, Peter H.
2 Seiler, Werner M.
2 Shankar, Natarajan
2 Ströder, Thomas
2 Sturm, Thomas
2 Tsitovich, Aliaksei
2 Weidenbach, Christoph
1 Ahrendt, Wolfgang
1 Albert, Elvira
1 Alberti, Francesco
1 Apt, Krzysztof Rafal
1 Avigad, Jeremy
1 Balat, Vincent
1 Barbosa, Haniel
1 Barrett, Clark W.
1 Barthe, Gilles
1 Bartocci, Ezio
1 Bax, Joshua
1 Beckert, Bernhard
1 Ben-Amram, Amir M.
1 Beringer, Lennart
1 Bobot, François
1 Borralleras, Cristina
1 Brauer, Jörg
1 Bridge, James P.
1 Brockschmidt, Marc
1 Bromberger, Martin
1 Burel, Guillaume
1 Cao, Zhenfu
1 Cauderlier, Raphaël
1 Chen, Jie
1 Cheng, Xi
1 Christ, Jürgen
1 Clarke, Edmund Melson jun.
1 Conchon, Sylvain
1 Cook, Byron
1 Corzilius, Florian
1 D’Argenio, Pedro Rubén
1 Desharnais, Jules
1 Devillers, Raymond
1 Diallo, Nafi
1 Din, Crystal Chang
1 Donaldson, Alastair F.
1 Dong, Xiaolei
1 Dross, Claire
1 Esen, Zafer
1 Esparza, Javier
1 Farooque, Mahfuza
1 Fietzke, Arnaud
1 Fiori, Alberto
...and 118 more Authors

Citations by Year