Verification of SMT systems with quantifiers

DOI10.1007/978-3-031-19992-9_10MaRDI QIDQ6160910zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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

• An automatic proving approach to parameterized verification
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Bounded quantifier instantiation for checking inductive invariants
• Decidability of parameterized verification
• Formal specification and verification of dynamic parametrized architectures
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• Infinite-state invariant checking with IC3 and predicate abstraction
• Property-directed inference of universal invariants or proving their absence
• Simplify: a theorem prover for program checking
• Solving quantified verification conditions using satisfiability modulo theories
• The MathSAT5 SMT solver
• Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning

Cited in

(15)

• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Global guidance for local generalization in model checking
• Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
• Bounded quantifier instantiation for checking inductive invariants
• Towards SMT Model Checking of Array-Based Systems
• scientific article; zbMATH DE number 5542982 (Why is no real title available?)
• Quantifier-free encoding of invariants for hybrid systems
• scientific article; zbMATH DE number 7577577 (Why is no real title available?)
• Light-weight SMT-based model checking
• Bounded quantifier instantiation for checking inductive invariants
• Quantifiers on demand
• QMaude: quantitative specification and verification in rewriting logic
• Invariant checking for SMT-based systems with quantifiers
• Deductive verification of alternating systems

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)