Philipp Rümmer
According to our database1, Philipp Rümmer
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
On csauthors.net:
Bibliography
2018
String constraints with concatenation and transducers solved efficiently.
PACMPL, 2018
Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report).
CoRR, 2018
2017
An Approximation Framework for Solvers and Decision Procedures.
J. Autom. Reasoning, 2017
Preface to special issue on satisfiability modulo theories.
Formal Methods in System Design, 2017
Exploring Approximations for Floating-Point Arithmetic using UppSAT.
CoRR, 2017
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report).
CoRR, 2017
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version).
CoRR, 2017
Fair Termination for Parameterized Probabilistic Concurrent Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017
Flatten and conquer: a framework for efficient analysis of string constraints.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017
Systematic Predicate Abstraction Using Variable Roles.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017
Quantified Heap Invariants for Object-Oriented Programs.
Proceedings of the LPAR-21, 2017
Abduction by Non-Experts.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017
Learning to prove safety over parameterised concurrent systems.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017
2016
Proof Search with Taclets.
Proceedings of the Deductive Software Verification - The KeY Book, 2016
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report).
CoRR, 2016
Guiding Craig interpolation with domain-specific abstractions.
Acta Inf., 2016
Regular Symmetry Patterns.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016
Deciding Bit-Vector Formulas with mcSAT.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016
Optimizing horn solvers for network repair.
Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016
JayHorn: A Framework for Verifying Java programs.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016
Characterization of Simulation by Probabilistic Testing.
Proceedings of the Theory and Practice of Formal Methods, 2016
2015
On recursion-free Horn clauses and Craig interpolation.
Formal Methods in System Design, 2015
Regular Symmetry Patterns (Technical Report).
CoRR, 2015
Efficient Algorithms for Bounded Rigid E-unification.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015
Automating Regression Verification.
Proceedings of the Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März, 2015
Conflict-Directed Graph Coverage.
Proceedings of the NASA Formal Methods - 7th International Symposium, 2015
Bixie: Finding and Understanding Inconsistent Code.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015
Free Variables and Theories: Revisiting Rigid E-unification.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015
Norn: An SMT Solver for String Constraints.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015
Theorem Proving with Bounded Rigid E-Unification.
Proceedings of the Automated Deduction - CADE-25, 2015
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.
Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, 2015
2014
Horn Clauses for Communicating Timed Systems.
Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014
The Gradual Verifier.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014
Automating regression verification.
Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014
String Constraints for Verification.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014
Approximations for Model Construction.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014
2013
Ranking function synthesis for bit-vector relations.
Formal Methods in System Design, 2013
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
CoRR, 2013
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
CoRR, 2013
Classifying and Solving Horn Clauses for Verification.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013
Joogie: from Java through Jimple to Boogie.
Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysis, 2013
Exploring interpolants.
Proceedings of the Formal Methods in Computer-Aided Design, 2013
Disjunctive Interpolants for Horn-Clause Verification.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
A Theory for Control-Flow Graph Exploration.
Proceedings of the Automated Technology for Verification and Analysis, 2013
2012
Craig Interpolation for the Integers: Results, Implementation, and Experiences.
Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012
E-Matching with Free Variables.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012
A Verification Toolkit for Numerical Transition Systems - Tool Paper.
Proceedings of the FM 2012: Formal Methods, 2012
Accelerating Interpolants.
Proceedings of the Automated Technology for Verification and Analysis, 2012
2011
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
J. Autom. Reasoning, 2011
Automatic analysis of DMA races using model checking and k-induction.
Formal Methods in System Design, 2011
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011
Software Verification Using k-Induction.
Proceedings of the Static Analysis - 18th International Symposium, 2011
SCRATCH: a tool for automatic analysis of dma races.
Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2011
Test-case generation for embedded simulink via formal concept analysis.
Proceedings of the 48th Design Automation Conference, 2011
2010
Practical Aspects of Automated Deduction for Program Verification.
KI, 2010
Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)
CoRR, 2010
A Polymorphic Intermediate Verification Language: Design and Logical Encoding.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010
Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010
Ranking Function Synthesis for Bit-Vector Relations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010
Interpolating Quantifier-Free Presburger Arithmetic.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010
Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010
Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays.
Proceedings of the 6th International Verification Workshop, 2010
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010
2009
Mutation-Based Test Case Generation for Simulink Models.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009
Real World Verification.
Proceedings of the Automated Deduction, 2009
2008
Integration of a security type system into a program logic.
Theor. Comput. Sci., 2008
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic.
Electr. Notes Theor. Comput. Sci., 2008
Non-termination Checking for Imperative Programs.
Proceedings of the Tests and Proofs, Second International Conference, 2008
Integrating Verification and Testing of Object-Oriented Software.
Proceedings of the Tests and Proofs, Second International Conference, 2008
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.
Proceedings of the Logic for Programming, 2008
2007
Construction of Proofs.
Proceedings of the Verification of Object-Oriented Software. The KeY Approach, 2007
Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic.
Proceedings of the Tests and Proofs, First International Conference, 2007
A Sequent Calculus for Integer Arithmetic with Counterexample Generation.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007
The KeY system 1.0 (Deduction Component).
Proceedings of the Automated Deduction, 2007
2006
Integration of a Security Type System into a Program Logic.
Proceedings of the Trustworthy Global Computing, Second Symposium, 2006
Sequential, Parallel, and Quantified Updates of First-Order Structures.
Proceedings of the Logic for Programming, 2006
Verifying Object-Oriented Programs with KeY: A Tutorial.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006
2005
Verification of JCSP Programs.
Proceedings of the 28th Communicating Process Architectures Conference, 2005