| Publication | Date of Publication | Type |
|---|
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
Formal Methods in System Design | 2025-01-13 | Paper |
| Expressiveness of extended bounded response \textsf{LTL} | 2024-12-06 | Paper |
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 |
A first-order logic characterisation of safety and co-safety languages
Lecture Notes in Computer Science | 2024-01-23 | Paper |
| Searching for ribbon-shaped paths in fair transition systems | 2024-01-23 | 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 |
Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans
(available as arXiv preprint) | 2023-10-02 | Paper |
A first-order logic characterization of safety and co-safety languages
Logical Methods in Computer Science | 2023-08-26 | Paper |
| SMT-based model checking of max-plus linear systems | 2023-08-21 | 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 |
Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis
Software Engineering and Formal Methods | 2023-05-26 | Paper |
Assumption-based runtime verification
Formal Methods in System Design | 2023-05-08 | 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 |
| Abstraction Modulo Stability for Reverse Engineering | 2022-12-07 | Paper |
\(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\)
Information Processing Letters | 2022-10-28 | Paper |
Safe decomposition of startup requirements: verification and synthesis
Tools and Algorithms for the Construction and Analysis of Systems | 2022-10-13 | Paper |
Diagnosability of fair transition systems
Artificial Intelligence | 2022-07-08 | 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 |
| 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 |
| Synthesis of P-stable abstractions | 2021-07-08 | Paper |
| Formal specification and verification of dynamic parametrized architectures | 2021-05-04 | Paper |
Computation of the transient in max-plus linear systems via SMT-solving
(available as arXiv preprint) | 2021-03-02 | 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 |
| From electrical switched networks to hybrid automata | 2020-01-03 | Paper |
Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
Computer Aided Verification | 2019-05-03 | Paper |
Mechanizing multi-agent reasoning with belief contexts
Practical Reasoning | 2019-04-29 | Paper |
Formal reliability analysis of redundancy architectures
Formal Aspects of Computing | 2019-03-13 | 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 |
Tightening the contract refinements of a system architecture
Formal Methods in System Design | 2018-08-08 | 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 |
Dynamic controllability via timed game automata
Acta Informatica | 2016-10-21 | Paper |
\textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Formal Verification of Infinite-State BIP Models
Automated Technology for Verification and Analysis | 2016-01-08 | Paper |
Formal safety assessment via contract-based design
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
HRELTL: a temporal logic for hybrid systems
Information and Computation | 2015-12-07 | Paper |
An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
Artificial Intelligence | 2015-11-18 | Paper |
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
Logical Methods in Computer Science | 2015-11-05 | Paper |
Efficient generation of Craig interpolants in satisfiability modulo theories
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Solving strong controllability of temporal problems with uncertainty using SMT
Constraints | 2015-04-29 | Paper |
Quantifier-free encoding of invariants for hybrid systems
Formal Methods in System Design | 2014-12-05 | Paper |
SMT-based scenario verification for hybrid systems
Formal Methods in System Design | 2014-03-28 | 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 |
Software model checking with explicit scheduler and symbolic threads
Logical Methods in Computer Science | 2012-08-15 | Paper |
Boosting Lazy Abstraction for SystemC with Partial Order Reduction
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 |
From sequential extended regular expressions to NFA with symbolic labels
Implementation and Application of Automata | 2011-02-11 | 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 |
Requirements Validation for Hybrid Systems
Computer Aided Verification | 2009-06-30 | 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 |
Verifying Heap-Manipulating Programs in an SMT Framework
Automated Technology for Verification and Analysis | 2008-07-03 | Paper |
Symbolic Fault Tree Analysis for Reactive Systems
Automated Technology for Verification and Analysis | 2008-07-03 | 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 |
SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA
International Journal of Foundations of Computer Science | 2008-05-20 | Paper |
Efficient Interpolant Generation in Satisfiability Modulo Theories
Tools and Algorithms for the Construction and Analysis of Systems | 2008-04-11 | Paper |
Diagnostic Information for Realizability
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Boolean Abstraction for Temporal Logic Satisfiability
Computer Aided Verification | 2007-11-29 | Paper |
A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis
Model Checking and Artificial Intelligence | 2007-11-01 | Paper |
Strong planning under partial observability
Artificial Intelligence | 2007-10-23 | Paper |
Symbolic Implementation of Alternating Automata
Implementation and Application of Automata | 2007-09-06 | 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 |
Formal Methods in Computer-Aided Design
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Weak, strong, and strong cyclic planning via symbolic model checking
Artificial Intelligence | 2006-02-07 | Paper |
Conformant planning via symbolic model checking and heuristic search
Artificial Intelligence | 2006-02-07 | 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 |
| scientific article; zbMATH DE number 2102731 (Why is no real title available?) | 2004-09-24 | 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 |
| scientific article; zbMATH DE number 1973987 (Why is no real title available?) | 2003-09-03 | Paper |
| scientific article; zbMATH DE number 1956570 (Why is no real title available?) | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1950649 (Why is no real title available?) | 2003-07-17 | Paper |
| scientific article; zbMATH DE number 1903365 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1746449 (Why is no real title available?) | 2002-05-28 | Paper |
| scientific article; zbMATH DE number 1701767 (Why is no real title available?) | 2002-02-05 | Paper |
| scientific article; zbMATH DE number 1560498 (Why is no real title available?) | 2001-06-04 | Paper |
| scientific article; zbMATH DE number 1552264 (Why is no real title available?) | 2001-01-15 | Paper |
NuSMV: A new symbolic model checker
International Journal on Software Tools for Technology Transfer. STTT | 2000-01-01 | Paper |
| Computational reflection via mechanized logical deduction | 1997-01-13 | Paper |
