Verification by approximate forward and backward reachability

• Main Authors: Govindaraju, Shankar G., Dill, David L.
• Format: Conference Proceeding
• Language: English
• Subjects: Algorithm design and analysis; Boolean functions; Computer systems organization > Architectures > Parallel architectures > Multiple instruction, multiple data; Computer systems organization > Dependable and fault-tolerant systems and networks; Contracts; Data structures; Formal verification; General and reference > Cross-computing tools and techniques > Performance; Government; Hardware; Laboratories; Lapping; Mathematics of computing > Mathematical analysis > Functional analysis > Approximation; Mathematics of computing > Mathematical software; Networks > Network performance evaluation; Permission; Theory of computation > Design and analysis of algorithms > Approximation algorithms analysis
• ISSN: 1092-3152
• DOI: 10.1145/288548.289055

Approximate reachability techniques trade off accuracy for the capacity to deal with bigger designs. In this paper, we extend the idea of approximations using overlapping projections to symbolic backward reachability. This is combined with a previous method of computing overapproximate forward reachable state sets using overlapping projections. The algorithm computes a superset of the set of states that lie on a path from the initial state to a state that violates a specified invariant property. If this set is empty, there is no possibility of violating the invariant. If this set is non-empty, it may be possible to prove the existence of such a path by searching for a counter-example. A simple heuristic is given, which seems to work well in practice, for generating a counter-example path from this approximation. We evaluate these new algorithms by applying them to several control modules from the I/O unit in the Stanford FLASH Multiprocessor.