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

DOI10.1007/978-3-030-79876-5_8OpenAlexW3182495053MaRDI QIDQ2055851

Gianluca Redondi, Alberto Griggio, Alessandro Cimatti

Publication date: 1 December 2021

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

zbMATH Keywords

parametric systemsSMTabstraction-refinementarray-based transitions systems

Mathematics Subject Classification ID

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

Related Items (5)

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

Uses Software

• z3
• CVC4
• Ivy
• Cubicle

Cites Work

• Unnamed Item
• Property-directed inference of universal invariants or proving their absence
• Formal specification and verification of dynamic parametrized architectures
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Infinite-state invariant checking with IC3 and predicate abstraction
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Towards SMT Model Checking of Array-Based Systems
• An Automatic Proving Approach to Parameterized Verification
• Formal Methods in Computer-Aided Design
• Eager abstraction for symbolic model checking

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