VCFloat: A Unified Coq Framework for Verifying C Programs with
Floating-Point Computations
Version 1.0 (2015-12-04)
Copyright (C) 2015 Reservoir Labs Inc.
All rights reserved.
patches/interval.patch is distributed under CeCILL-C, version 1.0. All
other files of this library are distributed under the GNU General
Public License, version 3.0, or (at your option) any later
version. See LICENSE for more legal information on use and
distribution of VCFloat.
For more technical information on VCFloat, you can read Sections 1 to
4 of our paper published at ACM/SIGPLAN Certified Programs and Proofs
(CPP) 2016:
Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
Lethin.
A Unified Coq Framework for Verifying C Programs with Floating-Point
Computations
Summary of directories (each of which corresponds to its logical path
with the same names where each path separator is replaced with . ):
vcfloat/cverif: Verification of CompCert Clight programs (separation
logic, etc.)
vcfloat: VCFloat reasoning framework and tactic
Most interesting files:
vcfloat/FPLang.v: VCFloat floating-point and annotated
floating-point calculus
vcfloat/FPLangOpt.v: further properties about VCFloat
vcfloat/Clight2FP.v: C to unannotated VCFloat
vcfloat/Clight2FPOpt.v: VCFloat annotation tactic
vcfloat/Example.v: examples of Section 4 of the abovementioned CPP
2016 paper (to be replayed interactively under ProofGeneral-Coq or
CoqIDE)
VCFloat requires Coq 8.5beta2.
VCFloat depends on the following further external libraries, which are
automatically downloaded from their official sources and built during
VCFloat's building process:
- Reservoir Labs Inc. R-CoqLib version 1.0 (from Reservoir Labs'
GitHub at http://github.com/reservoirlabs/rcoqlib )
- CompCert 2.4 (from AbsInt's GitHub at
https://github.com/AbsInt/CompCert.git , commit 5dd15440). VCFloat
contains a patch from this commit (patches/compcert.patch),
distributed under the GNU General Public License, version 3.0 or (at
your option) any later version.
- Ssreflect 1.5 (from its official website at
http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz )
- Mathematical Components (MathComp) 1.5 (from its official website at
http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz )
- Flocq 2.4.0 (from INRIA GForge at
https://gforge.inria.fr/git/flocq/flocq.git , commit bcbcde24)
- Coq-Interval 2.0.0 (from INRIA GForge at
https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git
, commit 81f1f918). VCFloat contains a patch from this commit
(patches/interval.patch), distributed under CeCILL-C, version 1.0.
See ACKS for copyright and licensing information about those external
libraries.
Usage: assuming that you already have a standard installation of Coq
8.5beta2, GNU make, GNU autoconf, GNU automake, and git.
0. Fetch the external libraries mentioned above, by running the
following automatic script:
./get_external_libs.sh
You can provide any further options that you want passed to the
`make' commands for Ssreflect and MathComp (e.g. -j)
1. Configure, by:
./configure
2. Build, by:
make
After building, you do not need to move the files anywhere else
(and, by the way, `make install' does not work). The build system
automatically generates a ./run-coqide.sh script to edit the sources
with CoqIDE (if installed on your system), as well as local load
path configuration files for Emacs+ProofGeneral (if installed on
your system). If you want to compile code against VCFloat, you can
have a look at the autogenerated `coqopts' file, to grab the load
path options to pass to Coq and its relevant tools (coqc,
coq_makefile, etc.)