| Publication | Date of Publication | Type |
|---|
On enumerating short projected models
Discrete Applied Mathematics | 2025-01-06 | Paper |
| On CNF conversion for disjoint SAT enumeration | 2024-11-26 | Paper |
Enhancing SMT-based weighted model integration by structure awareness
Artificial Intelligence | 2024-04-30 | 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 |
From \textsc{MiniZinc} to optimization modulo theories, and back
(available as arXiv preprint) | 2022-12-21 | Paper |
| Optimization modulo non-linear arithmetic via incremental linearization | 2022-03-24 | Paper |
Optimization modulo the theories of signed bit-vectors and floating-point numbers
Journal of Automated Reasoning | 2021-11-24 | Paper |
| Four flavors of entailment | 2021-04-07 | Paper |
Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results
Information and Computation | 2020-12-15 | 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 |
Optimization modulo the theory of floating-point numbers
(available as arXiv preprint) | 2020-03-10 | Paper |
\textsc{OptiMathSAT}: a tool for optimization modulo theories
Journal of Automated Reasoning | 2020-03-03 | Paper |
A new method for testing decision procedures in modal logics
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
Tools and Algorithms for the Construction and Analysis of Systems | 2019-09-17 | Paper |
Advanced SMT techniques for weighted model integration
Artificial Intelligence | 2019-08-28 | Paper |
Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
Automated Deduction — Cade-13 | 2019-01-15 | 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 |
| Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report | 2018-01-04 | Paper |
Satisfiability modulo transcendental functions via incremental linearization
(available as arXiv preprint) | 2017-09-22 | Paper |
Structured learning modulo theories
Artificial Intelligence | 2017-02-22 | Paper |
Colors Make Theories Hard
Automated Reasoning | 2016-09-05 | Paper |
Efficient generation of Craig interpolants in satisfiability modulo theories
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Optimization modulo theories with linear rational costs
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
| Encoding RTL constructs for \textsc{MathSAT}: a preliminary report | 2013-09-26 | Paper |
| Verifying industrial hybrid systems with \textsc{MathSAT} | 2013-09-20 | 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 |
Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
Automated Reasoning | 2012-09-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 |
Automated reasoning in \(\mathcal{ALCQ}\) via SMT
Lecture Notes in Computer Science | 2011-07-29 | 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 |
Journal on Data Semantics I
Lecture Notes in Computer Science | 2010-03-03 | Paper |
``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
Lecture Notes in Computer Science | 2010-02-05 | Paper |
Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability
Journal of Artificial Intelligence Research | 2009-12-10 | 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 |
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
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 |
From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain
Frontiers of Combining Systems | 2008-09-16 | Paper |
| Lazy satisfiability modulo theories | 2008-06-11 | 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 |
GSTE is partitioned model checking
Formal Methods in System Design | 2007-10-11 | Paper |
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ $\mathcal{ALC}$
Lecture Notes in Computer Science | 2007-09-04 | Paper |
Property-Driven Partitioning for Abstraction Refinement
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
Formal Methods for Hardware Verification
Lecture Notes in Computer Science | 2007-05-02 | Paper |
M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
Journal of Automated Reasoning | 2007-01-24 | Paper |
Efficient theory combination via Boolean search
Information and Computation | 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 |
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 |
| scientific article; zbMATH DE number 2090051 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2090300 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2086516 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2086590 (Why is no real title available?) | 2004-08-11 | Paper |
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
Journal of Applied Non-Classical Logics | 2004-01-11 | Paper |
| scientific article; zbMATH DE number 1973987 (Why is no real title available?) | 2003-09-03 | Paper |
| scientific article; zbMATH DE number 1946871 (Why is no real title available?) | 2003-07-07 | Paper |
| scientific article; zbMATH DE number 1903365 (Why is no real title available?) | 2003-05-01 | Paper |
Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
Information and Computation | 2003-01-14 | Paper |
| scientific article; zbMATH DE number 1765693 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1701755 (Why is no real title available?) | 2002-02-05 | Paper |
| scientific article; zbMATH DE number 1538056 (Why is no real title available?) | 2001-03-11 | Paper |
An analysis of empirical testing for modal decision procedures
Logic Journal of the IGPL | 2000-06-21 | Paper |
| scientific article; zbMATH DE number 1302390 (Why is no real title available?) | 1999-06-16 | Paper |
Calculating criticalities
Artificial Intelligence | 1998-07-23 | Paper |
scientific article; zbMATH DE number 1149437 (Why is no real title available?)
(available as arXiv preprint) | 1998-05-10 | Paper |
