Finding Model-Checkable Needles in Large Source Code Haystacks: Modular Bug-Finding via Static Analysis and Dynamic Invariant Discovery

TL;DR

This paper introduces a hybrid static and dynamic analysis approach to identify functions in large codebases that are suitable for model checking, leveraging invariants discovered from test suites to reduce false positives.

Contribution

It proposes a novel method combining static analysis and dynamic invariant discovery to find model-checkable functions in large, complex software systems.

Findings

Effective identification of functions with verifiable properties

Reduction of false positives through dynamic invariants

Scalability to large codebases despite poor test suites

Abstract

In this paper, we present a novel marriage of static and dynamic analysis. Given a large code base with many functions and a mature test suite, we propose using static analysis to find functions 1) with assertions or other evident correctness properties (e.g., array bounds requirements or pointer access) and 2) with simple enough control flow and data use to be amenable to predicate-abstraction based or bounded model checking without human intervention. Because most such functions in realistic software systems in fact rely on many input preconditions not specified by the language's type system (or annotated in any way), we propose using dynamically discovered invariants based on a program's test suite to characterize likely preconditions, in order to reduce the problem of false positives. While providing little in the way of verification, this approach may provide an additional quick and highly scalable bug-finding method for programs that are usually considered "too large to model check." We present a simple example showing that the technique can be useful for a more typically "model-checkable" code base, even in the presence of a poorly designed test suite and bad invariants.