Property-directed inference of universal invariants or proving their absence
From MaRDI portal
Publication:1702932
DOI10.1007/978-3-319-21690-4_40zbMath1381.68169OpenAlexW944431708MaRDI QIDQ1702932
Sharon Shoham, Nikolaj Bjørner, Aleksandr Karbyshev, Shachar Itzhaky, Noam Rinetzky
Publication date: 1 March 2018
Full work available at URL: https://doi.org/10.1007/978-3-319-21690-4_40
Related Items (8)
Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Horn Clause Solvers for Program Verification ⋮ Verification of SMT systems with quantifiers ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning
Uses Software
This page was built for publication: Property-directed inference of universal invariants or proving their absence
