| Publication | Date of Publication | Type |
|---|
Invariant checking for SMT-based systems with quantifiers
ACM Transactions on Computational Logic | 2024-11-12 | Paper |
| Efficient analysis of cyclic redundancy architectures via Boolean fault propagation | 2024-02-01 | Paper |
| Searching for i-good lemmas to accelerate safety model checking | 2024-01-12 | Paper |
Verification Modulo theories
Formal Methods in System Design | 2023-10-30 | Paper |
Verification of SMT systems with quantifiers
Automated Technology for Verification and Analysis | 2023-06-02 | Paper |
Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
Automated Technology for Verification and Analysis | 2023-06-02 | Paper |
| Analysis of cyclic fault propagation via ASP | 2023-04-04 | Paper |
\textsc{LTL} falsification in infinite-state systems
Information and Computation | 2022-12-08 | Paper |
Safe decomposition of startup requirements: verification and synthesis
Tools and Algorithms for the Construction and Analysis of Systems | 2022-10-13 | Paper |
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Logical Methods in Computer Science | 2022-10-06 | Paper |
| Automatic discovery of fair paths in infinite-state transition systems | 2022-06-22 | Paper |
| Implicit semi-algebraic abstraction for polynomial dynamical systems | 2022-03-25 | Paper |
| Optimization modulo non-linear arithmetic via incremental linearization | 2022-03-24 | Paper |
Certifying proofs for SAT-based model checking
Formal Methods in System Design | 2021-12-08 | Paper |
| Universal invariant checking of parametric systems with quantifier-free SMT reasoning | 2021-12-01 | Paper |
| Proving the existence of fair paths in infinite-state systems | 2021-10-18 | Paper |
Counterexample-guided prophecy for model checking modulo the theory of arrays
(available as arXiv preprint) | 2021-08-04 | Paper |
Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
Information and Computation | 2020-05-26 | Paper |
Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
Computer Aided Verification | 2019-05-03 | Paper |
Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
ACM Transactions on Computational Logic | 2018-10-24 | Paper |
| Experimenting on solving nonlinear integer arithmetic with incremental linearization | 2018-08-10 | Paper |
Satisfiability modulo transcendental functions via incremental linearization
(available as arXiv preprint) | 2017-09-22 | Paper |
Infinite-state invariant checking with IC3 and predicate abstraction
Formal Methods in System Design | 2017-07-26 | 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 |
\textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
Lecture Notes in Computer Science | 2016-08-30 | Paper |
A practical approach to satisfiability modulo linear integer arithmetic
Journal of Satisfiability, Boolean Modeling and Computation | 2016-02-23 | Paper |
Efficient generation of Craig interpolants in satisfiability modulo theories
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Deciding floating-point logic with abstract conflict driven clause learning
Formal Methods in System Design | 2014-12-05 | Paper |
An abstract interpretation of DPLL(T)
Lecture Notes in Computer Science | 2014-11-03 | Paper |
The MathSAT5 SMT solver
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
A modular approach to MaxSAT modulo theories
Theory and Applications of Satisfiability Testing – SAT 2013 | 2013-08-05 | Paper |
Efficient interpolant generation in satisfiability modulo linear integer arithmetic
Logical Methods in Computer Science | 2012-08-15 | Paper |
Stochastic local search for SMT: combining theory solvers with WalkSAT
Frontiers of Combining Systems | 2011-10-07 | Paper |
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Tools and Algorithms for the Construction and Analysis of Systems | 2011-05-19 | Paper |
Computing small unsatisfiable cores in satisfiability modulo theories
Journal of Artificial Intelligence Research | 2011-05-04 | Paper |
Satisfiability modulo the theory of costs: foundations and applications
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
Annals of Mathematics and Artificial Intelligence | 2009-11-16 | Paper |
Interpolant Generation for UTVPI
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Efficient Interpolant Generation in Satisfiability Modulo Theories
Tools and Algorithms for the Construction and Analysis of Systems | 2008-04-11 | Paper |
