Skip to content

1. Overview

Jump to bottom
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.

Clone this wiki locally