NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

A Library for Formal Verification of Low-level Programs

lib/stdlib_ext/: Small extensions to the standard libraries of Coq 8.3pl1 and ssreflect 1.3pl1. A file X_ext.v exports the standard library module X.
Arith_ext Bool_ext div_ext EqNat_ext Lists_ext Max_ext Reals_ext seq_ext ssrnat_ext String_ext ZArith_ext
lib/contrib/: Contributed libraries. They sometimes overlap with standard libraries but still provide new features. machine_int provides a formalization of finite-length integers (int : nat -> Type). finmap provides an original formalization of finite maps. Also contains Hoare-logic modules for a while-like language and a language with gotos (a formalization of [Ando Saabas and Tarmo Uustalu. A compositional natural semantics and Hoare logic for low-level languages. TCS 373(3):273--302, Elsevier, 2007]).
finmap listbit_correct listbit machine_int multi_int nodup omegaz order ordset_pairs ordset ssrrat string_c

Hoare logic modules:

compile goto sgoto_hoare sgoto while
seplog/: A formalization of separation logic [John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2002, IEEE]. Contains, as a use-case, a formal verification of the heap manager of an operating system [paper] and a certified verifier for a fragment of separation logic [paper].

Standard separation logic:

abst bipl example_reverse_list examples integral_type seplog syntax tactics

A certified verifier for a fragment of separation logic:

expr_b_dp frag_examples frag_list_entail frag_list_examples frag_list_init10 frag_list_init12 frag_list_init5 frag_list_max3 frag_list_reverse_list frag_list_swap frag_list_triple frag_list_vcg frag LSF_LWP_comparation

Formal verification of the heap manager of an operating system:

topsy_hmAlloc2 topsy_hmAlloc_example topsy_hmAlloc_prg topsy_hmAlloc topsy_hmFree_prg topsy_hmFree topsy_hmInit_prg topsy_hmInit topsy_hm topsy_threadBuild
cryptoasm/: A formalization of separation logic for the SmartMIPS assembly language. Contains applications to the formal verification of cryptographic functions (e.g., the Montgomery multiplication [paper], the BBS pseudorandom number generator [paper]).

Separation logic for SmartMIPS:

Asm encode_decode mapstos mips_bipl mips_cmd mips_contrib mips_frame mips_seplog mips_syntax mips_tactics

Illustrative example of SGoto:

compile_example sgoto_hoare_example

Formal verifications of cryptographic functions: program functional correctness other properties

seplogC/: A separation logic for the C language and its application to the formal verification of decoder functions of PolarSSL.

MinC:

C_bipl C_cmd C_examples C_expr C_pp_examples C_pp C_seplog C_types POLAR_asn1_get_len_pp POLAR_asn1_get_len POLAR_library_functions_pp POLAR_library_functions_triple POLAR_library_functions POLAR_parse_client_hello_pp POLAR_parse_client_hello_triple POLAR_parse_client_hello rfc5246
begcd/: A tentative formalization of simulations and its application to the formal verification of an assembly implementation of the binary extended gcd algorithm.

Toward Formal Construction of Assembly Arithmetic Functions from Pseudo-code:

begcd_mips_halve begcd_mips_init begcd_mips_prelude_prg begcd_mips_prelude begcd_mips_reset begcd_mips_subtract begcd_mips begcd library_interfaces multi_add_signed_unsigned_simu multi_div2_simu multi_is_even_and_prg multi_is_even_and_simu multi_is_even_simu multi_lt_simu multi_mul2_simu multi_sub_signed_signed_simu multi_sub_signed_unsigned_simu multi_zero_simu simu