Universal invariant checking of parametric systems with quantifier-free SMT reasoning

DOI10.1007/978-3-030-79876-5_8MaRDI QIDQ2055851zbMATH OpenOpenAlexFDO

Authors Alessandro Cimatti, Alberto Griggio, Gianluca Redondi

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_8

zbMATH Keywords

abstraction-refinementarray-based transitions systemsparametric systemsSMT

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Verification of SMT systems with quantifiers
• Abduction of trap invariants in parameterized systems
• On invariant synthesis for parametric systems
• scientific article; zbMATH DE number 1953016
• Parametric systems: verification and synthesis

Cites work

• An automatic proving approach to parameterized verification
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Eager abstraction for symbolic model checking
• Formal Methods in Computer-Aided Design
• 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
• Towards SMT Model Checking of Array-Based Systems
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning

Cited in

(6)

• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Verification Modulo theories
• Verification of SMT systems with quantifiers
• Invariant checking for SMT-based systems with quantifiers
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic

Describes a project that uses

Uses Software

• Ivy
• Cubicle
• z3
• CVC4

This page was built for publication: Universal invariant checking of parametric systems with quantifier-free SMT reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055851)