Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
From MaRDI portal
Abstract: The safety of infinite state systems can be checked by a backward reachability procedure. For certain classes of systems, it is possible to prove the termination of the procedure and hence conclude the decidability of the safety problem. Although backward reachability is property-directed, it can unnecessarily explore (large) portions of the state space of a system which are not required to verify the safety property under consideration. To avoid this, invariants can be used to dramatically prune the search space. Indeed, the problem is to guess such appropriate invariants. In this paper, we present a fully declarative and symbolic approach to the mechanization of backward reachability of infinite state systems manipulating arrays by Satisfiability Modulo Theories solving. Theories are used to specify the topology and the data manipulated by the system. We identify sufficient conditions on the theories to ensure the termination of backward reachability and we show the completeness of a method for invariant synthesis (obtained as the dual of backward reachability), again, under suitable hypotheses on the theories. We also present a pragmatic approach to interleave invariant synthesis and backward reachability so that a fix-point for the set of backward reachable states is more easily obtained. Finally, we discuss heuristics that allow us to derive an implementation of the techniques in the model checker MCMT, showing remarkable speed-ups on a significant set of safety problems extracted from a variety of sources.
Recommendations
Cited in
(24)- A unifying view on SMT-based software verification
- Superposition as a decision procedure for timed automata
- Formal specification and verification of dynamic parametrized architectures
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Combination of uniform interpolants via Beth definability
- Parameterized model checking on the TSO weak memory model
- On invariant synthesis for parametric systems
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
- Automated termination in model-checking modulo theories
- Verification of composed array-based systems with applications to security-aware workflows
- Decision procedures for flat array properties
- Towards SMT Model Checking of Array-Based Systems
- Goal-directed invariant synthesis for model checking modulo theories
- An extension of lazy abstraction with interpolation for programs with arrays
- Multi-parameterised compositional verification of safety properties
- SMT-based verification of data-aware processes: a model-theoretic approach
- Light-weight SMT-based model checking
- Predicate Abstraction in Program Verification: Survey and Current Trends
- MCMT: a model checker modulo theories
- Verification of SMT systems with quantifiers
- Synthesizing history and prophecy variables for symbolic model checking
- Invariant checking for SMT-based systems with quantifiers
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
This page was built for publication: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3081445)
