-
Notifications
You must be signed in to change notification settings - Fork 0
1. Overview
Murad Akhundov edited this page Aug 11, 2019
·
1 revision
This is a verification tool that attempts to speed up CBMC (can easily be adapted to work with other checkers) by isolating segments of the program and proving them separately when possible.
The program consists of the following components:
- CIL Plugins, written in OCaml using C Intermediate Language (found in
src/) - Command-line tool that runs the modules and the target verification tool, written in Typescript (found in
cli/) - Tests, written in Javascript with Mocha (found in
test/)
The CIL Modules can be used standalone to find and extract segments mentioned earlier.