Verification of SMT systems with quantifiers
From MaRDI portal
Publication:6160910
DOI10.1007/978-3-031-19992-9_10zbMATH Open1522.68303OpenAlexW4312481161MaRDI QIDQ6160910FDOQ6160910
Authors: Alessandro Cimatti, Alberto Griggio, Gianluca Redondi 
Publication date: 2 June 2023
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-031-19992-9_10
Recommendations
- Bounded quantifier instantiation for checking inductive invariants
- Bounded quantifier instantiation for checking inductive invariants
- Solving quantified verification conditions using satisfiability modulo theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Light-weight SMT-based model checking
Cites Work
- Simplify: a theorem prover for program checking
- The MathSAT5 SMT solver
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Infinite-state invariant checking with IC3 and predicate abstraction
- Title not available (Why is that?)
- Decidability of parameterized verification
- Solving quantified verification conditions using satisfiability modulo theories
- Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- An automatic proving approach to parameterized verification
- Property-directed inference of universal invariants or proving their absence
- Formal specification and verification of dynamic parametrized architectures
- Bounded quantifier instantiation for checking inductive invariants
Cited In (14)
- Title not available (Why is that?)
- Quantifiers on demand
- Bounded quantifier instantiation for checking inductive invariants
- Global guidance for local generalization in model checking
- Title not available (Why is that?)
- Bounded quantifier instantiation for checking inductive invariants
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Towards SMT Model Checking of Array-Based Systems
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Quantifier-free encoding of invariants for hybrid systems
- Invariant checking for SMT-based systems with quantifiers
- QMaude: quantitative specification and verification in rewriting logic
- Deductive verification of alternating systems
- Light-weight SMT-based model checking
This page was built for publication: Verification of SMT systems with quantifiers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160910)
