Examples of formal verification within Coq
The following verification examples are included in this repository
- remove.v
- filter.v
- split.v
To execute the examples:
- Download the Coq proof assistant here: (https://coq.inria.fr/download)
- Open CoqIDE
- File -> Open and navigate to one of the examples
- 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".