• Lecturer: Arthur Charguéraud

Slides:

• Introduction
• Chapter 1: see Coq script
• Chapter 2
• Chapter 3

Coq Binaries (cached here to save bandwidth):

• Windows: coq-installer-8.4-win-0.exe(install to c:\programs\coq, NOT to c:\program files\coq) and Msys for which you need to select the component “Msys” during the installation (install to C:\mingw).
• Mac OS: coqide-8.4rc1.dmg (Coq bundled with CoqIDE interface and some plugins: Ssreflect, AAC, Containers, DescenteInfinie).

Logic, Functional Programming, Type Systems, Hoare Logic.

• Specification and verification of purely functional programs
  • Terms and types in Coq
  • Definition of pure programs
  • Basic logic
  • Inductive reasoning
  • Specification and verification of functions
  • Examples: lists, batched queues, binary trees

• Specification of imperative programs
  • Interpretation of Separation Logic triples
  • Definition of Separation Logic predicates on heaps
  • Structural rules
  • Rules for reasoning about terms
  • Manipulation of heap predicates in Coq

• Verification of imperative programs using characteristic formulae
  • Construction of characteristic formulae
  • Treatment of functions
  • Integration of the structural rules
  • Tactics for munipulating characteristic formulae
  • Examples of verification of imperative programs

The course will contain lab sessions, for which you will need to bring a laptop equipped with a working installation of Coq v8.3 or Coq v8.4. It is usually more effective to work in pairs, so if you do not manage to install Coq you can pair up with someone else.

Under Linux or Mac/OS, try installing a packaged version of Coq, because the compilation of Coq and CoqIDE is not so straightforward (though some tips can be found on the Coq wiki). Under Windows, download the binary distribution from the Coq website and install Msys for compiling makefiles as explained in details in the README file in the zip archive.

Download the appropriate files, and make sure you read the README file in the archive:

• verif_linux_v8.3.tar.gz for Coq v8.3 under Linux
• verif_linux_v8.4.tar.gz for Coq v8.4 under Linux
• verif_linux_v8.4.tar.gz for Coq v8.4rc1 under Mac OS
• verif_win.zip for Coq v8.4 under Windows