| |
CS 246. Software Verification
|
|
|
|
|
Catalog description:
A
study of techniques to specify and verify the correctness of software
systems. Topics include formal specification, SAT and first order
theories, their decision processes and applications, program logics and
verification, mechanized verification, and program synthesis.
Summary:
Recent studies show that the global cost of software and hardware bugs
is hundreds of billion dollars annually. Aircraft, space shuttles,
self-driving cars, medical devices and Internet services are a few use
cases that require reliable systems. In the last decade, the
verification community has brought tools to assist engineers in
building reliable computing systems. We are at the beginning of the new
era of verified (rather than tested) computing products. The goal of
this course is to introduce the students to the theory and practice of
program specification and verification.
In this course, we will study propositional logic, first-order logic,
and commonly used first-order theories and their satisfiability
decision procedures. We will work with the state-of-the-art constraint
solving tools. We will also study programming using dependent types and
interactive theorem proving using higher order logics. We will work
with the state-of-the-art functional programming languages and theorem
provers. We will study Hoare logic to prove the partial and total
correctness of sequential programs. We also study abstract syntax,
operational semantics and basic type systems and their proof of
soundness. Finally. we will study the fundamentals of model checking.
Instructor:
Mohsen Lesani
Topics:
L for Lectures
D for Demos
L0. Introduction
L1. Propositional Logic
Suggested Reading:
Aaron Bradley and Zohar Manna. Chapter 1.1-1.5: Propositional Logic. Calculus of Computation. 2010.
L2. Basic SAT Solving
Suggested Reading:
Aaron Bradley and Zohar Manna. Chapter 1.6-1.7: Propositional Logic. Calculus of Computation. 2010.
L3. Modern SAT Solvers
Suggested Reading:
- Kroening, Daniel, and Ofer Strichman. Chapter 2.2. Decision procedures. Springer-Verlag Berlin Heidelberg, 2016.
- Joao Marques-Silva, Ines Lynce, and Sharad Malik. Chapter 4:
Conflict-Driven Clause Learning SAT Solvers. Handbook of
Satisfiability. 2008.
- Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman.
Chapter 2: Satisfiability Solvers. Handbook of Knowledge
Representation. 2008.
L4. Applications of SAT
Suggested Reading:
Edmund Clarke, Daniel Kroening, and Flavio Lerda. A Tool for Checking
ANSI-C Programs. Tools and Algorithms for the Construction and Analysis
of Systems (TACAS). 2004. Springer
L5. First order Logic
Suggested Reading:
Aaron Bradley and Zohar Manna. Chapter 2.1-2.4, 2-6-2.7: First-order Logic. Calculus of Computation. 2010.
D1. Introduction to verification in Coq
Software Foundations. Volume 1. Logical Foundations. Working with Structured Data (Lists)
https://softwarefoundations.cis.upenn.edu/
L6. SAT Modulo Theories
Suggested Reading:
- Aaron Bradley and Zohar Manna. Chapter 3: First-order Theories. Calculus of Computation. 2010.
- Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo
Theories: Introduction and Applications. Communications of the ACM,
vol. 54, no. 9. 2011.
L7. Theory of Equality
Suggested Reading:
Aaron Bradley and Zohar Manna. Chapter 9: Quantifier-Free Equality and Data Structures. Calculus of Computation. 2010.
L8. Combining Theories
Suggested Reading:
Aaron Bradley and Zohar Manna. Chapter 10: Combining Decision Procedures. Calculus of Computation. 2010.
L9. SMT Solvers
Suggested Reading:
Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare
Tinelli. Chapter 12: Satisfiability Modulo Theories. Handbook of
Satisfiability. 2008.
L10. Deductive Program Verification
Suggested Reading:
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10. 1969. ACM DL
- Aaron Bradley and Zohar Manna. Chapter 5: Program Correctness Mechanics. Calculus of Computation. 2010.
L11. Replication Coordination Analysis and Synthesis
Suggested Reading:
Hamsaz: Replication Coordination Analysis and Synthesis. Farzin
Houshmand, Mohsen Lesani, POPL'19 (ACM Symposium on Principles of
Programming Languages)
More to come if time allows:
Demo for Z3 SMT solver
Abstract Syntax and Operational Semantics
Type Systems and Type Soundness
Type Inference
Program Synthesis
Evaluation:
Midterm 1/3, Final 1/3, Project 1/3
Course material and lecture recordings will be provided to enrolled students.
|
|
|
|