Invariant inference with provable complexity from the monotone theory

DOI10.1007/978-3-031-22308-2_10MaRDI QIDQ6164427zbMATH OpenFDO

Authors Yotam M. Y. Feldman, Sharon Shoham

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2208.07451

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, but non-trivial upper bounds on the computational complexity of such algorithms are scarce, and limited to simple syntactic forms of invariants. In this paper we achieve invariant inference algorithms, in the domain of propositional transition systems, with provable upper bounds on the number of SAT calls. We do this by building on the monotone theory, developed by Bshouty for exact learning Boolean formulas. We prove results for two invariant inference frameworks: (i) model-based interpolation, where we show an algorithm that, under certain conditions about reachability, efficiently infers invariants when they have both short CNF and DNF representations (transcending previous results about monotone invariants); and (ii) abstract interpretation in a domain based on the monotone theory that was previously studied in relation to property-directed reachability, where we propose an efficient implementation of the best abstract transformer, leading to overall complexity bounds on the number of SAT calls. These results build on a novel procedure for computing least monotone overapproximations.

Recommendations

• Monotonicity inference for higher-order formulas
• Monotonicity inference for higher-order formulas
• Decidability of inferring inductive invariants
• Computer Science Logic
• Property-directed inference of universal invariants or proving their absence

Cites work

• A data driven approach for algebraic loop invariants
• A theory of formal synthesis via inductive learning
• A theory of the learnable
• Automatically inferring loop invariants via algorithmic learning
• Automating abstract interpretation
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
• Exact learning Boolean functions via the monotone theory
• From invariant checking to invariant inference using randomized search
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• scientific article; zbMATH DE number 2107521 (Why is no real title available?)
• scientific article; zbMATH DE number 3085175 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• On converting CNF to DNF
• Predicate abstraction for software verification
• Queries and concept learning
• SAT-Based Model Checking without Unrolling
• The octagon abstract domain
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Generalized compactness of nonmonotonic inference operations

This page was built for publication: Invariant inference with provable complexity from the monotone theory

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