资 源 简 介
Introduction
bp2bfg is a small command line program intended to translate Boolean programs to Boolean flow graphs, implemented in Ocaml. Both Boolean programs and Boolean flow graphs are formally defined, and the formal translation (not the implementation) is proven to be correct, i.e. the behaviour of a (initialized) Boolean program is the same as the behaviour of the corresponding (by the translation) initialized Boolean flow graph.
Boolean programs have been used before in different forms, and its original definition is due to Thomas Ball and Sriram K. Rajamani (2000). The Boolean flow graphs are defined as a part of the "Verification of Control-Flow Properties of Programs with Procedures"-project (CVPP for short). More information about CVPP can be found here. The syntax for Boolean programs that bp2bfg are using is currently slightly simplified and different from those used in other proje
