formalverif

Examples of formal verification within Coq

Examples

The following verification examples are included in this repository

• remove.v
• filter.v
• split.v

To execute the examples:

1. Download the Coq proof assistant here: (https://coq.inria.fr/download)
2. Open CoqIDE
3. File -> Open and navigate to one of the examples
4. Click the Green down arrow with a line below it to evaluate the entire file. When you hover over this green arrow, you should see "Go to end".