Description:
This course is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments and solver-aided languages that automatically verify logical arguments. We will learn how to apply these tools to certify that programs behave as expected. Specifically, we will look at 1. Formal logical reasoning about program correctness through 2. Coq proof assistant, a tool for machine checked mathematical theorem proving and 3. F*, a general-purpose programming language aimed at program verification.
Course Content:
- Foundations: Induction principles, logic and propositions, Curry-Howard
correspondence.
- Specification and Verification: Program Equivalence – Transition Systems –
Operational Semantics - Compiler Verification – Model Checking – Simply Typed
Lambda Calculus.
- Program Logics: Hoare logic: an approach to verifying imperative programs - Separation logic:
reasoning about aliasing and pointer-based data structures.
- Programming with F*: Programming in F* - Inductive Types -
Verified Functional Programming – Termination - Programming with Effects
- Proving with F*: Verifying Stateful Programs – Dijkstra Monad - Higher
Kinds, Indexed Types, Type-level functions – Cryptography examples - Verifying
low-level code using Low*, a subset of F*
- Concurrency: Concurrent Separation Logic and rely-guarantee reasoning:
verifying concurrent shared-memory programs - Pi-calculus and behavioral
refinement: modular reasoning about message-passing functional programs –
Session Types for distributed programming.
TextBooks:
Formal Reasoning about Programs, Adam Chlipala.
online.
ReferenceBooks:
- Software Foundations, Benjamin Pierce et al. Freely available online: https://softwarefoundations.cis.upenn.edu/
- Types and Programming Languages, Benjamin Pierce, MIT Press, 1st edition, 2002.
- Practical Foundations for Programming Languages, Robert Harper, Cambridge University Press, 2nd edition, 2016
