This course will introduce techniques for formal reasoning about programs and specifications. These techniques are fundamental to ensure that programs are correct and reliable. Bugs and insecurities in software have a huge societal cost, but ensuring programs correctness and reliability in practice is difficult. To assist programmers with this task, researcher in programming languages and software engineering have developed tools based on formal logic. The rigor of formal logic is useful to provide a formal specification for the program behaviour and to check, assisted by a machine, that the program meets this formal specification.
To introduce students to formal reasoning about programs and the basic techniques behind it we will use the Coq proof assistant and we will follow the approach developed in the online book Software Foundations. The precise schedule of the different classes will appear below.
The course has a significant component based on analysis of algorithms and systems, and formal techniques. So, the following are required classes: CAS CS 210, CAS CS 320 or equivalent; or consent of instructor. Additionally, some rudimentary understanding of formal logic is expected.
The course has two main requirements:
The final grade will be composed as follows:
In class and in the assignments we will use the proof assistant Coq. We recommend to install Coq using the Coq platform. More information are available here https://coq.inria.fr/download. We have also created a post on piazza to discuss problems with the installation that you may encounter.
|Tr 1/20|| No Class
|Tu 1/25||Introduction to the topic + Use of Coq + Basics