LASER 2011 Summerschool
Elba Island, Italy
Christine Paulin-Mohring
September 2011
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
A
T
E
X by
H
E
V
E
A
.