| Publication | Date of Publication | Type |
|---|
\textsc{Golem}: a flexible and efficient solver for constrained Horn clauses
Formal Methods in System Design | 2025-11-07 | Paper |
| Transition power abstractions for deep counterexample detection | 2024-01-23 | Paper |
| The \textsc{Golem} Horn solver | 2024-01-12 | Paper |
| Symbolic model checking for TLA+ made faster | 2023-12-13 | Paper |
Decomposing Farkas Interpolants
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
SMT-based verification of program changes through summary repair
Formal Methods in System Design | 2023-10-30 | Paper |
| Farkas-based tree interpolation | 2021-10-18 | Paper |
| A cooperative parallelization approach for property-directed \(k\)-induction | 2020-08-05 | Paper |
Exploiting partial variable assignment in interpolation-based model checking
Formal Methods in System Design | 2019-11-29 | Paper |
SMTS: Distributed, Visualized Constraint Solving
EPiC Series in Computing | 2019-07-04 | Paper |
Function summarization modulo theories
EPiC Series in Computing | 2019-07-04 | Paper |
Lookahead-Based SMT Solving
EPiC Series in Computing | 2019-07-04 | Paper |
Property directed equivalence via abstract simulation
Computer Aided Verification | 2019-05-03 | Paper |
| Lattice-based refinement in bounded model checking | 2018-12-07 | Paper |
Modeling for Verification
Handbook of Model Checking | 2018-07-20 | Paper |
| Theory refinement for program verification | 2017-11-15 | Paper |
A new acceleration-based combination framework for array properties
Frontiers of Combining Systems | 2017-02-27 | Paper |
OpenSMT2: an SMT solver for multi-core and cloud computing
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Decision procedures for flat array properties
Journal of Automated Reasoning | 2016-05-26 | Paper |
Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection
Lecture Notes in Computer Science | 2016-04-01 | Paper |
Automated discovery of simulation between programs
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Booster: an acceleration-based verification framework for array programs
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
Search-space partitioning for parallelizing SMT solvers
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Resolution proof transformation for compression and interpolation
Formal Methods in System Design | 2014-12-05 | Paper |
An extension of lazy abstraction with interpolation for programs with arrays
Formal Methods in System Design | 2014-12-05 | Paper |
Interpolation Properties and SAT-Based Model Checking
Automated Technology for Verification and Analysis | 2014-07-08 | Paper |
Loop summarization using state and transition invariants
Formal Methods in System Design | 2014-06-30 | Paper |
PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Definability of accelerated relations in a theory of arrays and its applications
Frontiers of Combining Systems | 2013-09-20 | Paper |
eVolCheck: incremental upgrade checker for C
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
A model checking-based approach for security policy verification of mobile systems
Formal Aspects of Computing | 2012-07-03 | Paper |
Lazy abstraction with interpolants for arrays
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Loop Summarization and Termination Analysis
Tools and Algorithms for the Construction and Analysis of Systems | 2011-05-19 | Paper |
An efficient and flexible approach to resolution proof reduction
Hardware and Software: Verification and Testing | 2011-04-06 | Paper |
Integrated Formal Methods
Lecture Notes in Computer Science | 2009-05-07 | Paper |
Loop Summarization Using Abstract Transformers
Automated Technology for Verification and Analysis | 2008-11-20 | Paper |
Verification of evolving software via component substitutability analysis
Formal Methods in System Design | 2008-07-30 | Paper |
Verification of Boolean programs with unbounded thread creation
Theoretical Computer Science | 2007-12-18 | Paper |
State/Event Software Verification for Branching-Time Specifications
Lecture Notes in Computer Science | 2007-11-29 | Paper |
Program Compatibility Approaches
Formal Methods for Components and Objects | 2007-09-11 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Model Checking Software
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Concurrent software verification with states, events, and deadlocks
Formal Aspects of Computing | 2006-10-25 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
FM 2005: Formal Methods
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Predicate abstraction of ANSI-C programs using SAT
Formal Methods in System Design | 2004-11-22 | Paper |
| scientific article; zbMATH DE number 1956497 (Why is no real title available?) | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1693529 (Why is no real title available?) | 2002-01-22 | Paper |
| scientific article; zbMATH DE number 1693453 (Why is no real title available?) | 2002-01-22 | Paper |
