Universal invariant checking of parametric systems with quantifier-free SMT reasoning
type: Item
instance of: scholarly article
title: Universal invariant checking of parametric systems with quantifier-free SMT reasoning
DOI: 10.1007/978-3-030-79876-5_8
author: Alessandro Cimatti
author: Alberto Griggio
author: Gianluca Redondi
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437076
zbMATH Keywords: parametric systems
zbMATH Keywords: array-based transitions systems
zbMATH Keywords: abstraction-refinement
zbMATH Keywords: SMT
describes a project that uses: Ivy
describes a project that uses: Cubicle
describes a project that uses: z3
describes a project that uses: CVC4
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 8
OpenAlex ID: W3182495053
cites work: Formal Methods in Computer-Aided Design
cites work: Infinite-state invariant checking with IC3 and predicate abstraction
cites work: Formal specification and verification of dynamic parametrized architectures
cites work: Towards SMT Model Checking of Array-Based Systems
cites work: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
cites work: Property-directed inference of universal invariants or proving their absence
cites work: An Automatic Proving Approach to Parameterized Verification
cites work: Counterexample-guided prophecy for model checking modulo the theory of arrays
cites work: Eager abstraction for symbolic model checking
cites work: Q2769579
description: scientific article; zbMATH DE number 7437076