| Publication | Date of Publication | Type |
|---|
| Enhancing active model learning with equivalence checking using simulation relations | 2024-03-11 | Paper |
| Certified reinforcement learning with logic guidance | 2023-08-28 | Paper |
| Synthesising programs with non-trivial constants | 2023-06-27 | Paper |
| Counterexample guided inductive synthesis modulo theories | 2023-05-26 | Paper |
| Abstract interpretation with unfoldings | 2022-08-12 | Paper |
| Lifting CDCL to Template-Based Abstract Domains for Program Verification | 2022-08-12 | Paper |
| Sound Numerical Computations in Abstract Acceleration | 2022-07-01 | Paper |
| Model checking boot code from AWS data centers | 2021-08-30 | Paper |
| Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration | 2021-06-09 | Paper |
| Deep reinforcement learning with temporal logics | 2021-03-02 | Paper |
| Learning the Language of Software Errors | 2020-05-14 | Paper |
| Automated formal synthesis of provably safe digital controllers for continuous plants | 2020-03-06 | Paper |
| Formalizing and checking thread refinement for data-race-free execution models | 2019-09-17 | Paper |
| Modular Demand-Driven Analysis of Semantic Difference for Program Versions | 2019-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5227061 | 2019-08-05 | Paper |
| DSValidator | 2018-12-06 | Paper |
| SAT-Based Model Checking | 2018-07-20 | Paper |
| Incremental bounded model checking for embedded software | 2017-11-29 | Paper |
| Unfolding-based Partial Order Reduction | 2017-09-12 | Paper |
| Periodic Orbits and Equilibria in Glass Models for Gene Regulatory Networks | 2017-07-27 | Paper |
| Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants | 2017-07-11 | Paper |
| Satisfiability checking and symbolic computation | 2017-06-21 | Paper |
| Decision procedures. An algorithmic point of view | 2017-03-30 | Paper |
| Independence Abstractions and Models of Concurrency | 2017-02-21 | Paper |
| Lost in abstraction: monotonicity in multi-threaded programs | 2016-12-22 | Paper |
| On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency | 2016-10-19 | Paper |
| $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation | 2016-08-30 | Paper |
| Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs | 2016-04-26 | Paper |
| Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs | 2016-04-26 | Paper |
| Automatic Generation of Propagation Complete SAT Encodings | 2016-03-23 | Paper |
| Learning the Language of Error | 2016-01-08 | Paper |
| Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration | 2015-10-02 | Paper |
| Deciding floating-point logic with abstract conflict driven clause learning | 2014-12-05 | Paper |
| Abstract conflict driven learning | 2014-11-27 | Paper |
| An Abstract Interpretation of DPLL(T) | 2014-11-03 | Paper |
| Abstraction of Syntax | 2014-11-03 | Paper |
| Lost in Abstraction: Monotonicity in Multi-threaded Programs | 2014-09-15 | Paper |
| Loop summarization using state and transition invariants | 2014-06-30 | Paper |
| Ranking function synthesis for bit-vector relations | 2014-06-30 | Paper |
| Model and Proof Generation for Heap-Manipulating Programs | 2014-04-16 | Paper |
| Abstract satisfaction | 2014-04-10 | Paper |
| Counterexample-guided abstraction refinement for symmetric concurrent programs | 2014-03-28 | Paper |
| Computing over-approximations with bounded model checking | 2013-09-26 | Paper |
| Making the most of BMC counterexamples | 2013-09-20 | Paper |
| Software Verification for Weak Memory via Program Transformation | 2013-08-05 | Paper |
| Counterexample-Guided Precondition Inference | 2013-08-05 | Paper |
| Efficient Coverability Analysis by Proof Minimization | 2012-09-25 | Paper |
| An interpolating sequent calculus for quantifier-free Presburger arithmetic | 2012-07-31 | Paper |
| Numeric Bounds Analysis with Conflict-Driven Learning | 2012-06-29 | Paper |
| Automatic analysis of DMA races using model checking and \(k\)-induction | 2012-03-09 | Paper |
| Linear Completeness Thresholds for Bounded Model Checking | 2011-08-19 | Paper |
| Loop Summarization and Termination Analysis | 2011-05-19 | Paper |
| Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic | 2011-02-15 | Paper |
| Strengthening Induction-Based Race Checking with Lightweight Static Analysis | 2011-02-15 | Paper |
| Mutation-Based Test Case Generation for Simulink Models | 2011-01-08 | Paper |
| Context-aware counter abstraction | 2010-11-03 | Paper |
| Interpolating Quantifier-Free Presburger Arithmetic | 2010-10-12 | Paper |
| An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic | 2010-09-14 | Paper |
| Verification and falsification of programs with loops using predicate abstraction | 2010-05-05 | Paper |
| Ranking Function Synthesis for Bit-Vector Relations | 2010-04-27 | Paper |
| Correct Hardware Design and Verification Methods | 2010-02-05 | Paper |
| Interpolant Strength | 2010-01-14 | Paper |
| A framework for satisfiability modulo theories | 2009-11-13 | Paper |
| Finding Lean Induced Cycles in Binary Hypercubes | 2009-07-07 | Paper |
| Symbolic Counter Abstraction for Concurrent Software | 2009-06-30 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
| A First Step Towards a Unified Proof Checker for QBF | 2009-03-10 | Paper |
| Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers | 2009-02-24 | Paper |
| Loop Summarization Using Abstract Transformers | 2008-11-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3515554 | 2008-07-29 | Paper |
| Approximation Refinement for Interpolation-Based Model Checking | 2008-04-04 | Paper |
| Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant | 2008-02-27 | Paper |
| Verification of Boolean programs with unbounded thread creation | 2007-12-18 | Paper |
| An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors | 2007-11-29 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-28 | Paper |
| Deciding Bit-Vector Arithmetic with Abstraction | 2007-09-03 | Paper |
| Verification of SpecC using predicate abstraction | 2007-06-21 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-05-02 | Paper |
| Model Checking Software | 2006-11-01 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2005-11-10 | Paper |
| Computer Aided Verification | 2005-08-25 | Paper |
| Computer Aided Verification | 2005-08-25 | Paper |
| Predicate abstraction of ANSI-C programs using SAT | 2004-11-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4414397 | 2003-07-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4946042 | 2000-03-22 | Paper |
