| Publication | Date of Publication | Type |
|---|
An active learning approach to synthesizing program contracts
| 2024-06-05 | Paper |
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
| 2024-04-26 | Paper |
On strings in software model checking
| 2024-04-19 | Paper |
Probabilistic bisimulation for parameterized systems (with applications to verifying anonymous protocols)
Computer Aided Verification | 2024-02-16 | Paper |
OptiRica: towards an efficient optimizing Horn solver
| 2024-02-16 | Paper |
Automatic program instrumentation for automatic verification
| 2024-02-01 | Paper |
Decision procedures for sequence theories
| 2024-01-12 | Paper |
Regular model checking revisited
Model Checking, Synthesis, and Learning | 2023-05-26 | Paper |
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
1517.68074 | 2022-12-22 | Paper |
Monadic decomposition in integer linear arithmetic
| 2022-11-09 | Paper |
Reasoning in the theory of heap: satisfiability and interpolation
| 2022-03-23 | Paper |
scientific article; zbMATH DE number 7453201 (Why is no real title available?)
| 2022-01-06 | Paper |
scientific article; zbMATH DE number 7453198 (Why is no real title available?)
| 2022-01-06 | Paper |
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Formal Methods in System Design | 2021-12-08 | Paper |
Horn clauses for communicating timed systems
| 2021-06-28 | Paper |
Characterization of simulation by probabilistic testing
| 2021-05-20 | Paper |
Fair termination for parameterized probabilistic concurrent systems
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Liveness of randomised parameterised systems under arbitrary schedulers
Computer Aided Verification | 2019-05-03 | Paper |
Quantified Heap Invariants for Object-Oriented Programs
EPiC Series in Computing | 2019-01-10 | Paper |
Exploring approximations for floating-point arithmetic using UppSAT
| 2018-10-18 | Paper |
Automating regression verification of pointer programs by predicate abstraction
Formal Methods in System Design | 2018-07-16 | Paper |
An approximation framework for solvers and decision procedures
Journal of Automated Reasoning | 2017-07-10 | Paper |
Free variables and theories: revisiting rigid \(E\)-unification
Frontiers of Combining Systems | 2017-02-27 | Paper |
Deciding Bit-Vector Formulas with mcSAT
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Guiding Craig interpolation with domain-specific abstractions
Acta Informatica | 2016-06-28 | Paper |
Regular symmetry patterns
Lecture Notes in Computer Science | 2016-03-23 | Paper |
Efficient algorithms for bounded rigid \(E\)-unification
Lecture Notes in Computer Science | 2015-12-11 | Paper |
Theorem proving with bounded rigid \(E\)-unification
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
On recursion-free Horn clauses and Craig interpolation
Formal Methods in System Design | 2015-10-20 | Paper |
Approximations for Model Construction
Automated Reasoning | 2014-09-26 | Paper |
A theory for control-flow graph exploration
Automated Technology for Verification and Analysis | 2014-07-08 | Paper |
Ranking function synthesis for bit-vector relations
Formal Methods in System Design | 2014-06-30 | Paper |
Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
Electronic Notes in Theoretical Computer Science | 2014-01-10 | Paper |
Accelerating interpolants
Automated Technology for Verification and Analysis | 2012-11-21 | Paper |
An interpolating sequent calculus for quantifier-free Presburger arithmetic
Journal of Automated Reasoning | 2012-07-31 | Paper |
E-matching with free variables
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Automatic analysis of DMA races using model checking and \(k\)-induction
Formal Methods in System Design | 2012-03-09 | Paper |
Beyond quantifier-free interpolation in extensions of Presburger arithmetic
Lecture Notes in Computer Science | 2011-02-15 | Paper |
Mutation-Based Test Case Generation for Simulink Models
Formal Methods for Components and Objects | 2011-01-08 | Paper |
Interpolating quantifier-free Presburger arithmetic
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
An interpolating sequent calculus for quantifier-free Presburger arithmetic
Automated Reasoning | 2010-09-14 | Paper |
Ranking function synthesis for bit-vector relations
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
A polymorphic intermediate verification language: design and logical encoding
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
Real World Verification
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Integration of a Security Type System into a Program Logic
Trustworthy Global Computing | 2009-03-05 | Paper |
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Integration of a security type system into a program logic
Theoretical Computer Science | 2008-08-06 | Paper |
Sequential, Parallel, and Quantified Updates of First-Order Structures
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Non-termination Checking for Imperative Programs
Tests and Proofs | 2008-04-24 | Paper |
Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
Tests and Proofs | 2007-10-31 | Paper |
scientific article; zbMATH DE number 2177623 (Why is no real title available?)
| 2005-06-21 | Paper |
