Infinite-state invariant checking with IC3 and predicate abstraction

DOI10.1007/s10703-016-0257-4zbMath1368.68245OpenAlexW2522207775WikidataQ62041091 ScholiaQ62041091MaRDI QIDQ2363814

Stefano Tonetta, Alessandro Cimatti, Sergio Mover, Alberto Griggio

Publication date: 26 July 2017

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-016-0257-4

zbMATH Keywords

model checkinginfinite-state systemsSMTpredicate abstractionIC3inductive invariants

Mathematics Subject Classification ID

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

Related Items (24)

Improving Generalization in Software IC3 ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Software Verification with PDR: An Implementation of the State of the Art ⋮ Safe Decomposition of Startup Requirements: Verification and Synthesis ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Incremental design-space model checking via reusable reachable state approximations ⋮ Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems ⋮ SMT-based generation of symbolic automata ⋮ Verification Modulo theories ⋮ Unnamed Item ⋮ Towards a dereversibilizer: fewer asserts, statically ⋮ Verification of SMT systems with quantifiers ⋮ A unifying view on SMT-based software verification ⋮ Unnamed Item ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ Model-based safety assessment of a triple modular generator with xSAP ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning ⋮ Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction* ⋮ On the combination of polyhedral abstraction and SMT-based model checking for Petri nets ⋮ Abstraction-based incremental inductive coverability for Petri nets

Uses Software

• PVS
• MathSAT5
• InvGen
• nuXmv
• PKind
• Kind 2
• JKind
• Tip
• GitHub
• CTIGAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Property-directed inference of universal invariants or proving their absence
• Infinite-state invariant checking with IC3 and predicate abstraction
• Generalized Property Directed Reachability
• Efficient generation of craig interpolants in satisfiability modulo theories
• SAT-Based Model Checking without Unrolling
• Abstractions from proofs
• Counterexample-guided abstraction refinement for symbolic model checking
• SMT-Based Induction Methods for Timed Systems
• Property Directed Polyhedral Abstraction
• Lazy abstraction
• The MathSAT5 SMT Solver
• Computer Aided Verification
• Lazy Abstraction with Interpolants

This page was built for publication: Infinite-state invariant checking with IC3 and predicate abstraction