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