Welcome to Introduction to Formal Methods
CS5860 - Fall 2014 course
Formal methods is an area of computer science concerned with using computers to help with the intellectual tasks of designing, specifying, and building software and hardware. Elements of that work include using formal logic to write specifications and prove that programs and processes implement them.
The subject originated in the area of computer science that we call Artificial Intelligence (AI), where the pioneering researchers such as John McCarthy, Alan Newell, Herbert Simon, Robin Milner and many others designed and implemented computer systems to carry out formal proofs. Some projects employed automatic theorem provers which attempted to find proofs on their own. Other projects built interactive proof assistants to help users construct proofs. Related projects implemented model checkers to systematically look for errors in programs and specifications. This course will focus on interactive proof assistants.
The subject gradually made a significant impact on programming languages because programs and proofs of their correctness could be built together. By now there are numerous examples of software tools that are proven correct. For example, the CompCert C compiler built by Xavier Leroy and his group is the only C compiler for which the Csmith tool designed to find bugs cannot find any wrong-code errors. The Paris metro (line 14) driverless train uses verified software. By 1971 it was discovered that efficient programs could be compiled from formal constructive proofs – much of that work was done here at Cornell. It is now a flourishing area of research worldwide done both in academia and in industry. This work relies heavily on proof assistants such as Coq, Nuprl, Agda, MetaPRL, HOL, and others. The Coq prover is being used to develop the book Software Foundations in which all of the mathematical results about software are formally proved. The Spec# program development system helps users of C# write programs that are documented by proved assertions written in-line.
Formal methods are critically needed in the area of distributed computing because the key protocols used by industry are extremely complex and difficult to specify and code correctly. The challenge in designing and building asynchronous computing systems is due in large part to the incredible number of possible interactions among processes – so many that the unaided human mind cannot imagine all the possible ways in which these protocols can go wrong. This makes modern computing systems highly vulnerable to cyber-attack. We will examine this area in the last section of the course.
The course material will be in the lecture notes and assigned readings from the original literature. There will be demonstrations of the Coq and Nuprl proof assistants and perhaps other formal tools, and some students might elect to use them in projects.
Tentative Topics and Lectures Outline
- Formal Methods
- Historical perspective
- Formal systems
- Programming languages
- Specification languages and logics
- Proof assistants
- Syntax of formulas
- Evidence and truth
- Inductive types and relations
- Automation of proof
- Correct-by-construction programming
- SAT and SMT solvers
- State and commands
- State monad
- Hoare logic
- Applications in databases and cyber physical systems
- Process model of computation
- Consensus protocols and impossibility results
- Correct-by-construction protocols
- Applications to cybersecurity
320 Gates Hall
Office Hours: After class and by appointment
Time: Mon/Weds 10:10AM - 11:25AM
Location: Upson 211