Introduction to Formal Verification course at CS Club

Building HTML files locally

Setup Alectryon using its installation instructions and add it to your PATH. (You need Alectryon v1.1 or newer).
Run make or make doc in the project root directory.

Classes

Class 1

Intro to formal verification slides
Intro to functional programming in Coq: source, rendered
No seminar
Homework: hw01.v

Class 2

Polymorphic functions & Dependent functions, Implicit Arguments, Notations, Product types and sum types: source, rendered
Seminar: seminar01.v
Homework: hw02.v

Class 3

Defining logic, equality. Dependent pattern matching: source, rendered
Seminar: seminar02.v
Homework: hw03.v

Class 4

Injectivity and disjointness of constructors, large elimination. Convoy pattern. Proofs by induction. Prop vs Type: source, rendered
Seminar: seminar03.v
Homework: hw04.v

Class 5

SSReflect tactic language source, rendered
Seminar: seminar04.v
Homework: hw05.v

Class 6

Proofs by induction: source, rendered
SSReflect proof methodology slides
Seminar: seminar05.v
Homework: hw06.v

Class 7

Views. reflect-predicate. Multi-rewrite rules: source, rendered
Seminar: seminar06.v
Homework: hw07.v

Class 8

Canonical Structures & Hierachies slides
Canonical Structures & Hierachies: demo (source), demo (rendered)
Seminar: seminar07.v
Homework: hw08.v

Class 9

Verification of insertion sort and merge sort. Non-structurally recursive functions. Nested fix pattern. Program plugin. Acc-predicate. source, rendered
Seminar: seminar08.v
Homework: hw09.v

Class 10

A potpourri of tools: automation (linear integer arithmetic, hammers), Equations plugin, property based randomized testing, mutation proving, extraction source, rendered
Seminar: seminar09.v
Homework: no homework

Awesome exercise solutions by class participants

unit_neq_bool solution and generalization by @kana-sama
A compiler from a language of arithmetic expressions to a stack language: solution and generalization by @kana-sama