Verification Modulo theories

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)

zbMATH Keywords

formal verificationmodel checkingsatisfiability modulo theoriesinfinite-state transition systemsimplicit predicate abstraction

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

First order Büchi automata and their application to verification of LTL specifications

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

This page was built for publication: Verification Modulo theories