The following pages link to Philipp Rümmer (Q300416):
Displayed 45 items.
- Guiding Craig interpolation with domain-specific abstractions (Q300418) (← links)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic (Q438556) (← links)
- On recursion-free Horn clauses and Craig interpolation (Q746767) (← links)
- Automatic analysis of DMA races using model checking and \(k\)-induction (Q763238) (← links)
- Integration of a security type system into a program logic (Q935469) (← links)
- Automating regression verification of pointer programs by predicate abstraction (Q1650864) (← links)
- Exploring approximations for floating-point arithmetic using UppSAT (Q1799086) (← links)
- Characterization of simulation by probabilistic testing (Q2026807) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Monadic decomposition in integer linear arithmetic (Q2096441) (← links)
- Reasoning in the theory of heap: satisfiability and interpolation (Q2119112) (← links)
- Ranking function synthesis for bit-vector relations (Q2248069) (← links)
- An approximation framework for solvers and decision procedures (Q2362497) (← links)
- Regular Symmetry Patterns (Q2796070) (← links)
- Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
- Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic (Q2871841) (← links)
- E-Matching with Free Variables (Q2891467) (← links)
- Free Variables and Theories: Revisiting Rigid E-unification (Q2964448) (← links)
- (Q3021903) (← links)
- Mutation-Based Test Case Generation for Simulink Models (Q3066126) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Approximations for Model Construction (Q3192205) (← links)
- Fair Termination for Parameterized Probabilistic Concurrent Systems (Q3303911) (← links)
- Theorem Proving with Bounded Rigid E-Unification (Q3454123) (← links)
- Efficient Algorithms for Bounded Rigid E-unification (Q3455762) (← links)
- Ranking Function Synthesis for Bit-Vector Relations (Q3557080) (← links)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (Q3557085) (← links)
- Integration of a Security Type System into a Program Logic (Q3608456) (← links)
- Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Q4633552) (← links)
- Quantified Heap Invariants for Object-Oriented Programs (Q4645747) (← links)
- Accelerating Interpolants (Q4649296) (← links)
- Interpolating Quantifier-Free Presburger Arithmetic (Q4933327) (← links)
- (Q4997235) (← links)
- (Q5020659) (← links)
- (Q5020662) (← links)
- A Theory for Control-Flow Graph Exploration (Q5166718) (← links)
- Real World Verification (Q5191121) (← links)
- Sequential, Parallel, and Quantified Updates of First-Order Structures (Q5387908) (← links)
- Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic (Q5423862) (← links)
- Non-termination Checking for Imperative Programs (Q5458816) (← links)
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic (Q5505560) (← links)
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (Q5747778) (← links)
- Regular model checking revisited (Q6045028) (← links)
- Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols) (Q6194589) (← links)
- (Q6197214) (← links)