Verification Modulo theories
From MaRDI portal
Publication:6056642
DOI10.1007/s10703-023-00434-xMaRDI QIDQ6056642
Alberto Griggio, Marco Roveri, Sergio Mover, Stefano Tonetta, Alessandro Cimatti
Publication date: 30 October 2023
Published in: Formal Methods in System Design (Search for Journal in Brave)
formal verificationmodel checkingsatisfiability modulo theoriesinfinite-state transition systemsimplicit predicate abstraction
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier-free encoding of invariants for hybrid systems
- Model-based safety assessment of a triple modular generator with xSAP
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- \textsc{LTL} falsification in infinite-state systems
- Automatic discovery of fair paths in infinite-state transition systems
- SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
- Proving the existence of fair paths in infinite-state systems
- Formal semantics and verification of network-based biocomputation circuits
- Infinite-state invariant checking with IC3 and predicate abstraction
- Solving Non-linear Arithmetic
- Efficient generation of craig interpolants in satisfiability modulo theories
- SAT-Based Model Checking without Unrolling
- Applying Linear Quantifier Elimination
- Abstractions from proofs
- Counterexample-guided abstraction refinement for symbolic model checking
- Solving SAT and SAT Modulo Theories
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
- SMT-Based Induction Methods for Timed Systems
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Lazy abstraction
- Predicate Abstraction via Symbolic Decision Procedures
- The MathSAT5 SMT Solver
- Verification of Timed Automata via Satisfiability Checking
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
