Formal Methods

We will explore mathematical techniques for improving software
reliability, namely for specifying and reasoning about properties of
software and tools for helping validate these properties.


(1) basic tools from logic for making and justifying precise claims
about programs;

(2) the use of proof assistants (hybrid tools that try to automate the
more routine aspects of building proofs while depending on human
guidance for more difficult aspects) to construct rigorous logical
arguments;

(3) the idea of functional programming, both as a method of
programming and as a bridge between programming and logic;

(4) formal techniques for reasoning about the properties of specific
programs (e.g., that a loop terminates on all inputs, or that a
sorting function actually fulfills its specification), using Hoare logics and

(5) the use of type systems for establishing well-behavedness
guarantees for all programs in a given programming language (e.g., the
fact that well-typed Java programs cannot be subverted at runtime). The system under study will be the simply-typed lambda calculus

Finally we will look at current research geared towards better automation
i. Connection with automated theorem provers (CoqHammer)
ii. machine learning

The specificity of this course is that is based around Coq which
provides a rich environment for interactive development of
machine-checked formal reasoning. The kernel of the Coq system is a
simple proof-checker which guarantees that only correct deduction
steps are performed. On top of this kernel, the Coq environment
provides high-level facilities for proof development. All the course
is formalized and machine-checked: It is intended to be read alongside
an interactive session with Coq.