| Publication | Date of Publication | Type |
|---|
Enhancing active model learning with equivalence checking using simulation relations
Formal Methods in System Design | 2024-03-11 | Paper |
Certified reinforcement learning with logic guidance
Artificial Intelligence | 2023-08-28 | Paper |
Synthesising programs with non-trivial constants
Journal of Automated Reasoning | 2023-06-27 | Paper |
Counterexample guided inductive synthesis modulo theories
Computer Aided Verification | 2023-05-26 | Paper |
Abstract interpretation with unfoldings
(available as arXiv preprint) | 2022-08-12 | Paper |
Lifting CDCL to template-based abstract domains for program verification
Automated Technology for Verification and Analysis | 2022-08-12 | Paper |
Lifting CDCL to template-based abstract domains for program verification
Automated Technology for Verification and Analysis | 2022-08-12 | Paper |
Sound Numerical Computations in Abstract Acceleration
Numerical Software Verification | 2022-07-01 | Paper |
Model checking boot code from AWS data centers
Formal Methods in System Design | 2021-08-30 | Paper |
Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
Journal of Automated Reasoning | 2021-06-09 | Paper |
| Deep reinforcement learning with temporal logics | 2021-03-02 | Paper |
Learning the language of software errors
Journal of Artificial Intelligence Research | 2020-05-14 | Paper |
Automated formal synthesis of provably safe digital controllers for continuous plants
Acta Informatica | 2020-03-06 | Paper |
Formalizing and checking thread refinement for data-race-free execution models
(available as arXiv preprint) | 2019-09-17 | 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
Static Analysis | 2019-09-16 | Paper |
| scientific article; zbMATH DE number 7088727 (Why is no real title available?) | 2019-08-05 | Paper |
DSValidator: an automated counterexample reproducibility tool for digital systems
Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) | 2018-12-06 | Paper |
SAT-Based Model Checking
Handbook of Model Checking | 2018-07-20 | Paper |
Incremental bounded model checking for embedded software
Formal Aspects of Computing | 2017-11-29 | Paper |
Unfolding-based partial order reduction
(available as arXiv preprint) | 2017-09-12 | Paper |
Periodic Orbits and Equilibria in Glass Models for Gene Regulatory Networks
IEEE Transactions on Information Theory | 2017-07-27 | Paper |
Sound and automated synthesis of digital stabilizing controllers for continuous plants
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control | 2017-07-11 | Paper |
Satisfiability checking and symbolic computation
ACM Communications in Computer Algebra | 2017-06-21 | Paper |
Satisfiability checking and symbolic computation
ACM Communications in Computer Algebra | 2017-06-21 | Paper |
Decision procedures. An algorithmic point of view
Texts in Theoretical Computer Science. An EATCS Series | 2017-03-30 | Paper |
Independence abstractions and models of concurrency
Lecture Notes in Computer Science | 2017-02-21 | Paper |
Lost in abstraction: monotonicity in multi-threaded programs
Information and Computation | 2016-12-22 | Paper |
On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
Formal Techniques for Distributed Objects, Components, and Systems | 2016-10-19 | Paper |
\textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Unrestricted termination and non-termination arguments for bit-vector programs
Programming Languages and Systems | 2016-04-26 | Paper |
Propositional reasoning about safety and termination of heap-manipulating programs
Programming Languages and Systems | 2016-04-26 | Paper |
Automatic generation of propagation complete SAT encodings
Lecture Notes in Computer Science | 2016-03-23 | Paper |
Learning the Language of Error
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
Static Analysis | 2015-10-02 | Paper |
Deciding floating-point logic with abstract conflict driven clause learning
Formal Methods in System Design | 2014-12-05 | Paper |
Abstract conflict driven learning
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
An abstract interpretation of DPLL(T)
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Abstraction of syntax
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Lost in abstraction: monotonicity in multi-threaded programs
CONCUR 2014 – Concurrency Theory | 2014-09-15 | Paper |
Loop summarization using state and transition invariants
Formal Methods in System Design | 2014-06-30 | Paper |
Ranking function synthesis for bit-vector relations
Formal Methods in System Design | 2014-06-30 | Paper |
Model and proof generation for heap-manipulating programs
Programming Languages and Systems | 2014-04-16 | Paper |
Abstract satisfaction
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Counterexample-guided abstraction refinement for symmetric concurrent programs
Formal Methods in System Design | 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
Programming Languages and Systems | 2013-08-05 | Paper |
Counterexample-guided precondition inference
Programming Languages and Systems | 2013-08-05 | Paper |
Efficient coverability analysis by proof minimization
Lecture Notes in Computer Science | 2012-09-25 | Paper |
An interpolating sequent calculus for quantifier-free Presburger arithmetic
Journal of Automated Reasoning | 2012-07-31 | Paper |
Numeric bounds analysis with conflict-driven learning
Tools and Algorithms for the Construction and Analysis of Systems | 2012-06-29 | Paper |
Automatic analysis of DMA races using model checking and \(k\)-induction
Formal Methods in System Design | 2012-03-09 | Paper |
Linear completeness thresholds for bounded model checking
Computer Aided Verification | 2011-08-19 | Paper |
Loop Summarization and Termination Analysis
Tools and Algorithms for the Construction and Analysis of Systems | 2011-05-19 | Paper |
Beyond quantifier-free interpolation in extensions of Presburger arithmetic
Lecture Notes in Computer Science | 2011-02-15 | Paper |
Strengthening induction-based race checking with lightweight static analysis
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 |
Context-aware counter abstraction
Formal Methods in System Design | 2010-11-03 | 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 |
Verification and falsification of programs with loops using predicate abstraction
Formal Aspects of Computing | 2010-05-05 | Paper |
Ranking function synthesis for bit-vector relations
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
Correct Hardware Design and Verification Methods
Lecture Notes in Computer Science | 2010-02-05 | Paper |
Interpolant strength
Lecture Notes in Computer Science | 2010-01-14 | Paper |
A framework for satisfiability modulo theories
Formal Aspects of Computing | 2009-11-13 | Paper |
Finding Lean Induced Cycles in Binary Hypercubes
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Symbolic Counter Abstraction for Concurrent Software
Computer Aided Verification | 2009-06-30 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
A First Step Towards a Unified Proof Checker for QBF
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
Computing Binary Combinatorial Gray Codes Via Exhaustive Search With SAT Solvers
IEEE Transactions on Information Theory | 2009-02-24 | Paper |
Loop Summarization Using Abstract Transformers
Automated Technology for Verification and Analysis | 2008-11-20 | Paper |
| Towards a classification of Hamiltonian cycles in the 6-cube | 2008-07-29 | Paper |
Approximation Refinement for Interpolation-Based Model Checking
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
Texts in Theoretical Computer Science. An EATCS Series | 2008-02-27 | Paper |
Verification of Boolean programs with unbounded thread creation
Theoretical Computer Science | 2007-12-18 | Paper |
An Algebraic Algorithm for the Identification of Glass Networks with Periodic Orbits Along Cyclic Attractors
Algebraic Biology | 2007-11-29 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Deciding Bit-Vector Arithmetic with Abstraction
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Verification of SpecC using predicate abstraction
Formal Methods in System Design | 2007-06-21 | 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 |
Computer Aided Verification
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 |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Predicate abstraction of ANSI-C programs using SAT
Formal Methods in System Design | 2004-11-22 | Paper |
| scientific article; zbMATH DE number 1953038 (Why is no real title available?) | 2003-07-25 | Paper |
| scientific article; zbMATH DE number 1421020 (Why is no real title available?) | 2000-03-22 | Paper |
