> uberSpark (Composable Verification of Commodity System Software) Documentation
Software Requirements and Dependencies
We assume your are working in:
<home-dir> with your home-directory name and
any working directory of your choice.
- Ubuntu 14.04.2 LTS 64-bit for development and verification
You will need to install the following packages after doing an update:
- OPAM (OCaml Package Manager)
- coq proof assistant (8.6.1)
- Frama-C (version Phosphorus-20170501)
- Install CVC3, Alt-Ergo and Z3 as backend theorem provers. The WP Frama-C plugin
manual (available here)
contains a chapter on installing the theorem provers.