Travelled to:1 × Canada
1 × Cyprus
1 × France
1 × Russia
1 × Sweden
1 × Switzerland
1 × United Kingdom
2 × Austria
2 × Germany
3 × Italy
4 × USA
Collaborated with:D.Kröning A.W.Lin A.F.Donaldson C.M.Wintersteiger P.Backeman L.Holík V.Klebanov M.Schäf A.Zeljic H.Hojjat V.Kuncak A.Brillout T.Wahl K.R.M.Leino H.Velroyen M.A.Shah P.A.Abdulla M.F.Atig Y.Chen A.Rezine T.McCarthy N.He A.Platzer J.Quesel J.Stenman L.Haller B.Cook C.Engel C.Gladisch T.Kahsai H.Sanchez C.Hong R.Majumdar D.Felsing S.Grebing M.Ulbrich Petr Janku T.Vojnar T.Chen M.Hague Z.Wu F.Konecný F.Garnier R.Iosif B.Beckert M.Giese R.Hähnle S.Schlager P.H.Schmitt Bui Phi Diep
Talks about:verif (8) string (5) constraint (4) program (4) analysi (4) system (4) interpol (3) arithmet (3) use (3) framework (2)
Person: Philipp Rümmer
DBLP: R=uuml=mmer:Philipp
Facilitated 1 volumes:
EdContributed to:
2015
2015
2015
20142014
20142013
2012
2011
2011
2011
20112010
20102009
2008200720072016201620182019
2017
20182019Wrote 28 papers:
- CADE-2015-BackemanR #bound #proving #theorem proving
- Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
- CAV-2015-AbdullaACHRRS #constraints #named #smt #string
- Norn: An SMT Solver for String Constraints (PAA, MFA, YFC, LH, AR, PR, JS), pp. 462–469.
- ICSE-v2-2015-McCarthyRS #comprehension #consistency #named
- Bixie: Finding and Understanding Inconsistent Code (TM, PR, MS), pp. 645–648.
- ASE-2014-FelsingGKRU #automation #verification
- Automating regression verification (DF, SG, VK, PR, MU), pp. 349–360.
- CAV-2014-AbdullaACHRRS #constraints #string #verification
- String Constraints for Verification (PAA, MFA, YFC, LH, AR, PR, JS), pp. 150–166.
- IJCAR-2014-ZeljicWR #approximate
- Approximations for Model Construction (AZ, CMW, PR), pp. 344–359.
- CAV-2013-RummerHK #verification
- Disjunctive Interpolants for Horn-Clause Verification (PR, HH, VK), pp. 347–363.
- FM-2012-HojjatKGIKR #tool support #verification
- A Verification Toolkit for Numerical Transition Systems — Tool Paper (HH, FK, FG, RI, VK, PR), pp. 247–251.
- DAC-2011-HeRK #concept analysis #embedded #generative #testing
- Test-case generation for embedded simulink via formal concept analysis (NH, PR, DK), pp. 224–229.
- PPoPP-2011-DonaldsonKR #analysis #automation #named
- SCRATCH: a tool for automatic analysis of dma races (AFD, DK, PR), pp. 311–312.
- SAS-2011-DonaldsonHKR #using #verification
- Software Verification Using k-Induction (AFD, LH, DK, PR), pp. 351–368.
- VMCAI-2011-BrilloutKRW #quantifier
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (AB, DK, PR, TW), pp. 88–102.
- IJCAR-2010-BrilloutKRW #calculus #quantifier
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (AB, DK, PR, TW), pp. 384–399.
- TACAS-2010-CookKRW #ranking #synthesis
- Ranking Function Synthesis for Bit-Vector Relations (BC, DK, PR, CMW), pp. 236–250.
- TACAS-2010-DonaldsonKR #analysis #automation #manycore #memory management
- Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors (AFD, DK, PR), pp. 280–295.
- TACAS-2010-LeinoR #design #encoding #logic #polymorphism #verification
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (KRML, PR), pp. 312–327.
- CADE-2009-PlatzerQR #verification
- Real World Verification (AP, JDQ, PR), pp. 485–501.
- TAP-2008-EngelGKR #object-oriented #testing #verification
- Integrating Verification and Testing of Object-Oriented Software (CE, CG, VK, PR), pp. 182–191.
- TAP-2008-VelroyenR #imperative #source code
- Non-termination Checking for Imperative Programs (HV, PR), pp. 154–170.
- CADE-2007-BeckertGHKRSS #component #deduction
- The KeY system 1.0 (Deduction Component) (BB, MG, RH, VK, PR, SS, PHS), pp. 379–384.
- TAP-2007-RummerS #calculus #java #logic #proving #source code #using
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic (PR, MAS), pp. 41–60.
- CAV-2016-KahsaiRSS #framework #java #named #source code #verification
- JayHorn: A Framework for Verifying Java programs (TK, PR, HS, MS), pp. 352–358.
- CAV-2016-LinR #liveness #random
- Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (AWL, PR), pp. 112–133.
- IJCAR-2018-ZeljicBWR #approximate #float #using
- Exploring Approximations for Floating-Point Arithmetic Using UppSAT (AZ, PB, CMW, PR), pp. 246–262.
- CAV-2019-HongLMR #bisimulation #probability #protocol #verification
- Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols) (CDH, AWL, RM, PR), pp. 455–474.
- PLDI-2017-AbdullaACDHRR #analysis #constraints #framework #performance #string
- Flatten and conquer: a framework for efficient analysis of string constraints (PAA, MFA, YFC, BPD, LH, AR, PR), pp. 602–617.
- POPL-2018-HolikJLRV #constraints #string #transducer
- String constraints with concatenation and transducers solved efficiently (LH, PJ, AWL, PR, TV), p. 32.
- POPL-2019-ChenHLRW #source code #string
- Decision procedures for path feasibility of string-manipulating programs with complex operations (TC, MH, AWL, PR, ZW), p. 30.