Vmc is a project mainly written in OCaml, based on the BSD-3-Clause license.
Verified Multicore C
VFMC (Verified Featherweight Multicore C) is a fragment of C enriched with asynchronous memory operations and fork/join primitives, together with function pre-conditions and post-conditions and loop invariants. VFMC aims to serve as an experimental intermediate language for verification of multicore C programs. Possible uses include verification for heterogeneous architectures with a host CPU and a number of accelerator cores (such as IBM Cell Broadband Engine) or verification of GPU (e.g., CUDA, OpenCL) programs.
To run the build process, call: $ make build
This will generate the following executable file for vfmc: ./bin/vfmc
To set the environment variables necessary for vfmc to run: $ . setenv
To run all of the tests in the examples directory: $ make test
Dependencies: