COURSE 2018
From Monday January 22 to Friday January 26, 2018, Yves Bertot will be teaching a
course entitled
“SOFTWARE VERIFICATION AND COMPUTER PROOF”
in the context of the international computer science master at the university of Nice, in Sophia Antipolis.
This course is also supported by Université Côte d’Azur
PROGRAM
1/ Basic programming with Coq’s functional programming language.
- Course notes available here, Course examples available here
- Slides (borrowed from Enrico Tassi), Demo, Exercises, Solutions
2/ Handling logical formulas and performing basic proofs.
3/ Reasoning about recursive functions.
4/ Proofs in arithmetic and execution of formally verified programs
5/ General datatypes
Courses will take place from Monday 13:30 to Friday 12:00 (the other days of the week 9:00 to 12:00 and 13:30 to 17:00) and will alternate lectures with hands-on exercises for all students. The course is in English and will be located at Inria Sophia Antipolis, in room K1 (Global coordinates: 43.61544,7.06811). You should ask for directions at the entrance of the Inria research center.
This course is an introductory course intended for students in computer science who have very little knowledge of functional programming and no knowledge of computer proof. The background in mathematics will also be elementary (basically, you are required to know how to perform a division on a sheet of paper).
At the end of the week, we expect that students will know how to write little programs (for instance number or list manipulations), write specifications about programs (for instance that a sorting algorithm does not loose data), and perform the proof that programs satisfy specifications. If you, one of your students, or one of your colleagues wishes to learn about Coq from scratch, this may be the right event for you.
If you are a doctoral student in computer science or mathematics, not already specializing in computer-based proofs, you will be able to validate credits for this course, as long as you show up to most of the sessions during the week.
We expect anybody attending to come with a laptop computer on which a recent version of Coq has been installed, either from pre-compiled versions (as provided by Debian or other Linux distributions) or as re-compiled from the sources, available on the site of the Coq system.
This course is for free, thanks to the support provided by Inria and Université Côte d’Azur. If you wish to attend, it is preferable that you send a mail to Yves Bertot and Nathalie Bellesso (both mail addresses are firstname.name@inria.fr ), so that I can plan the size of the required room and I can warn you about changes in the organization. For accommodation, you will have to take care of it individually, but information is available on the page on accommodation.
