LASER 2011 Summerschool
Elba Island, Italy

Documentation

• Course notes
• Slides introduction
• Slides course 1 Exercise on propositional logic Solution
• Slides course 2 Board example
• Slides course 3 Examples of recursive definitions
• Slides course 4 loop recursion monadic constructions
• Slides course 5 tactic language and reflection

Challenges

• max, sum and linear search : Coq source code HTML version
• linked lists : Coq source code HTML version
• n-queens : Coq source code, HTML version
• Needham-Schroeder Public Key protocol :
  • Version with flaw : Coq source code, HTML version
  • Corrected version : Coq source code, HTML version

Software

Software demonstrated during this course

• Coq version 8.3 Web site Reference Manual
• External Coq libraries:
  • Floating point numbers Flocq
  • Reasoning on reals using intervals Interval tactic
• External tools:
  • Frama-C : analysis of C programs (Web site).
  • Why : program deductive analysis Web site, new generation Why3 (Web site).
  • Gappa : tool to analyse floating point computation Web site with an associated Coq library
  • Alt-ergo an SMT prover for program verification (Web site).

Bibliography

• Some references

This document was translated from L^AT_EX by H^EV^EA.