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

doi:10.1007/978-3-032-10794-7_20

Return

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

2026-01-01

PRE

L Losavio

Marco Paganoni *

Carlo A. Furia

DOI：10.1007/978-3-032-10794-7_20

Original

Original request for help

Save

Abstract

En 中文

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, such validation techniques 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 Boogies 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 Boogies 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.

Keywords:

FORMAL VERIFICATION