Welcome to x86proved
x86proved is a Coq library that supports modelling, specification, generation, and proof for x86 machine code programs.
Requirements
To use x86proved you will need
- The Coq proof assistant, version 8.4
- The ssreflect tactic language and library, version 1.4
- A Coq development environment such as CoqIDE or emacs + Proof General
You can obtain all three bundled for 32-bit and 64-bit Windows from
Pierre-Yves Strub's web page.
You will need either
- On Windows: nmake.exe, supplied with Visual Studio, versions of which you can download for free
- On Unix/Cygwin: make
Install
Under construction
Contribute
There are many ways to contribute to x86proved.
- Extend the model to cover more features of x86 e.g. instructions, floating point, 64-bit, SIMD, paging, multi-core
- Improve the automation of proofs
- Languages
Documentation
Under construction