Navigating the Coq Development

WiSE is a symbolic execution based bug finder implemented an proven correct in Coq. Coq is a purely functional programming language that can also be used as a proof assistant to formalize mathematics and prove theorems. This document aims at guiding the readers through the Coq sources of WiSE.

How to read WiSE sources

The source code of WiSE is composed of 3 sorts of objects: code that can be executed, mathematical definitions, and mathematical proofs.

Code and definitions

Code and mathematical definitions are written in the purely functional language of Coq, and resembles OCaml, Haskell or any other functional language. For example, an inductive data type definition looks like this:

        
Inductive expr : Type :=
  | Var (s : string)
  | Add (e1 e2 : expr)
  | ...

Functions are defined using the keywords Definition or Fixpoint (for recursive functions). Below are 2 examples of function definitions :

        
Definition Double (e : expr) : expr := Add e e.

Fixpoint eq_expr (e1 e2 : expr) : bool :=
  match e1, e2 with
  | Var s1, Var s2 => s1 =? s2
  | ...

Theorems and proofs

Theorems and their proofs start with the keyword Theorem or Lemma, followed by the name of the theorem, and then followed by a proof script.

        
Lemma eq_expr_correct:
  forall e1 e2, eq_expr e1 e2 = true <-> e1 = e2.
Proof.
  induction e1, e2.
  ...
Qed.

Note that proof scripts are not necessarily meant to be read. When the sources are compiled, the Coq compiler checks the validity of all proofs.

How to navigate WiSE sources

To navigate the Coq sources, we strongly recommend to use the interactive web documentation and to go through the following selection of files in this order (from top to bottom):

Module Name	Type of source	Description
WiSE.lang.imp	code	The definition of the target programming language IMP (AST)
WiSE.lang.imp	definitions	A mathematical description of IMP’s execution model (concrete semantics)
WiSE.symbolic.symex	definitions	A mathematical description of IMP’s symbolic execution model (symbolic semantics)
WiSE.symbolic.symex	proofs	A formal proof that the symbolic execution model is consistent with respect to the concrete one
WiSE.implem.bugfinder	code	A purely functional and executable implementation of a bug finder based on the symbolic execution model
WiSE.implem.bugfinder_proof	proofs	A proof that the bug finder implementation only finds true bugs and can eventually discover all bugs

The other Coq files contain auxillary definitions that are not relevant to the understanding of the development. Nonetheless, all files are extensively documented