Schedule

• Info is available on the S2 schedule

Teachers

• Antoine Gontard (antoine.gontard@inria.fr)
• Raphaël Berthon (rberthon@lmf.cnrs.fr)

Part 1: SAT exercises

• Exercise sheet
• Skeleton files
• Sudoku missing file
• Ocamlc makefile (without print)

Part 2 : Rocq tutorial

• Useful links:
  • Do not hesitate to ask questions to Rocq users and developpers on the zulip
  • Here is the reference manual and in particular the tactic index
  • For the most basic and important tactics, you are encouraged to search “coq cheatsheet” or “rocq cheatsheet” (you will get different results) and pick whichever fits you best. Here is for example one the one used in M2 MPRI.
• Sheet

Séance 1

propositional.v
firstorder.v

Séance 2

Diaporama introduction à CIC
nats.v
inductives.v

Séance 3

lists.v
CORRECTION of measure.v (modified only after line 80)
acc.v

Séance 4

decidability.v
extraction.v

Séance 5

A solution of measure.v

Part 3 : Rocq project: a verified SAT solver

• instructions pdf and its associated bootstrap.v file
• Beware that april 6th is a national holiday, so this project spans across 3 mondays!

Evaluation

Out of 20 total points for this course:

• 3 come from the SAT exercises (Due February 15th - extended). If the files are too heavy (because of the examples), only send the files you had to change, which should much lighter.
• 10 come from the Rocq project (Due April 19th)
• 7 come from the DPLL project (Due May 10th)

Aknowledgement

This iteration of the course is strongly inspired by the 2024-25 iteration by Nicolas Margulies and Théo Vignon, itself strongly inspired by the 2020-21 iteration by David Baelde.