Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics

TL;DR

This paper presents BCC, a model-based testing approach that uses executable operational semantics to identify bugs in the Boogie intermediate verifier by generating and executing random programs.

Contribution

It introduces BCC, combining formal semantics with program generation to test and validate the Boogie verifier, revealing potential bugs and completeness issues.

Findings

Generated 3 million Boogie programs for testing

Found 2% of cases indicating completeness failures

Demonstrated effectiveness of lightweight testing for formal tools

Abstract

Lightweight validation technique, such as those based on random testing, are sometimes practical alternatives to full formal verification -- providing valuable benefits, such as finding bugs, without requiring a disproportionate effort. In fact, they can be useful even for fully formally verified tools, by exercising the parts of a complex system that go beyond the reach of formal models. In this context, this paper introduces BCC: a model-based testing technique for the Boogie intermediate verifier. BCC combines the formalization of a small, deterministic subset of the Boogie language with the generative capabilities of the PLT Redex language engineering framework. Basically, BCC uses PLT Redex to generate random Boogie programs, and to execute them according to a formal operational semantics; then, it runs the same programs through the Boogie verifier. Any inconsistency between the two executions (in PLT Redex and with Boogie) may indicate a potential bug in Boogie's implementation. To understand whether BCC can be useful in practice, we used it to generate three million Boogie programs. These experiments found 2% of cases indicative of completeness failures (i.e., spurious verification failures) in Boogie's toolchain. These results indicate that lightweight analysis tools, such as those for model-based random testing, are also useful to test and validate formal verification tools such as Boogie.