A technique for automata-based verification with residual reasoning

Abstract

Analysing programs at a high-level of abstraction reduces the effort required for verification, but may abstract away details required for full verification of a specification. Working at a lower level, e.g. through model checking or runtime verifying program code, can avoid this problem of abstraction, at the expense of much larger resource requirements. To reduce the resources required by verification, analysis techniques at decreasing levels of abstraction can be combined in a complementary manner through partial verification or residual analysis, where any useful partial information discovered at a high-level is used to reduce the verification problem, leaving an easier residual problem for lower-level analyses. Our contribution in this paper is a technology-agnostic symbolic-automata-based framework to project verification effort onto different verification stages. Properties and programs are both represented as symbolic automata, with an event-based view of verification. We give correctness conditions for residual analysis based on equivalence with respect to verification of the original problem. Furthermore we present an intraprocedural residual analysis to identify parts of the property respected by the program, and parts of the program that cannot violate the property.