Program of the 3rd Asian-Pacific Summer School on Formal Methods
Lecturers
| Lecturer | Institution |
|---|---|
| Yves Bertot | INRIA Sophia Antipolis, Microsoft Research-INRIA Joint Centre, Orsay |
| Pierre Casteran | Université de Bordeaux I |
| Sandrine Blazy | University of Rennes I |
| Chris Hawblitzel | Microsoft Research |
| Zhong Shao | Yale University |
| Xinyu Feng | University of Science and Technology of China |
Preliminary Program
- August 13:
- 08:45-08:50 : Opening (Xinyu Feng) [pdf video-A]
08:50-10:15 : Introduction to Coq (Yves) [pdf video-A B mp3]
10:30-12:00 : Propositional logic in Coq (Pierre) [pdf video-A B mp3]
14:00: Exercises on Coq - August 14:
- 08:45-10:15 : Programming on natural numbers and lists in Coq (Yves) [pdf video-A B mp3]
- 10:30-12:00 : First-order logic and equality in Coq (Pierre) [pdf video-A B mp3]
- 14:00: Exercises on Coq
- August 15:
- 08:45-10:15 : Inductive types in Coq (Pierre) [pdf video-A B mp3]
- 10:30-12:00 : Proofs by induction on natural numbers (Yves) [pdf video-A B mp3]
- 14:00: Exercises on Coq
- August 16:
- 08:45-10:15 : Recursive functions in Coq (Yves) [pdf video-A B mp3]
- 10:30-12:00 : Inductive predicates in Coq (Pierre) [pdf demos video-A B mp3]
- 14:00: Exercises on Coq
- August 17:
- 08:45-10:15 : Proof techniques for inductive types and inductive predicates (Pierre) [pdf demos Video-A B C mp3]
- 10:30-12:00 : Introduction to dependent types in Coq (Yves) [pdf Video-A B mp3]
- 14:00: Exercises on Coq
- August 18:
- 08:45-10:15 : Overview of advanced features in Coq (Pierre) [pdf demos Video-A B mp3]
- 10:30-12:00 : Mechanizing language semantics in Coq (Yves) [pdf demos Video-A B mp3]
- 14:00: Exercises on Coq
- August 19:
- 08:45-12:00 : CompCert: formal verification of a realistic C compiler (Sandrine) [pdf demo Video-A B C D mp3]
- afternoon : Tour to Tongli, a beautiful town (with rivers, lakes and gardens) in Suzhou [Photos]
- evening : Dinner
- August 20:
- 08:45-12:00 : Using Mechanized Reasoning to Verify Operating System Code (Chris) [ppt]
- 14:00-15:30 : Advanced Development of Certified System Software (Zhong) [ppt]
- 16:00-17:30 : Separation Logic and Concurrency Verification (Xinyu) [ppt]
- August 21:
- Workshop on Proof Assistants in Formal Methods