2024FA - PROG LANG&CMPILRS I 16:198:515:01

This course serves as an introduction to the field of formal methods for programming languages, aiming to equip students with the knowledge and skills necessary for constructing highly reliable software. Formal methods hinge on the precise specification of run-time properties that software systems are expected to meet. The foundation of these methods lies in expressing specifications in languages characterized by formal syntax, semantics, and theory.
 
Key Aspects and Benefits of Formal Methods:
 
1. Precision and Clarity:
   - Formal methods naturally lead to unambiguous and high-quality specifications.
   - The use of formal languages improves the clarity of specifications.
 
2. Automation and Tool Support:
   - Formality serves as the basis for developing automated tools that support the software development process.
   - Automated verification tools help identify errors in requirements, models, designs, and implementations.
 
Throughout the course, students will achieve the following learning objectives:
   - Gain knowledge about the role of formal methods (FMs) in programming languages.
   - Understand how formal methods contribute to the creation of high-quality programming systems.
   - Learn about formal modeling and specification languages.
   - Acquire the ability to write and comprehend formal requirement specifications.
   - Explore main approaches in formal software verification.
   - Use formal verification tools to verify models and code.
 
Tentative Topics to Cover:
  - Type checking and inference
  - Refinement type systems 
  - Abstract interpretation 
  - SMT solvers 
  - Hoare logics, verification conditions, and invariant inference
  - Modern tools e.g. Dafny, Spacer, LiquidTypes, Ivy, and Z3

Working with OCaml:
  - Please either install the OCaml compiler following the instructions https://ocaml.org/docs/installing-ocaml or directly use iLab.

Office Hours:
  - Wednesdays 4-5 pm

Lectures