3 credits
Fall 2025 Lecture Distance Learning Upper Division
The course focuses on the logical foundations and algorithmic techniques used to ensure program correctness. With an emphasis on automated program verification and synthesis, the course covers classical concepts and techniques such as Hoare logic, abstract interpretation, abstraction-refinement and bounded model checking. The course also exposes students to approaches for program synthesis, a new frontier for program reasoning, such as inductive synthesis, synthesis using version space algebras, constraint-based synthesis and synthesis based on machine-learning techniques. The courses emphasizes both theoretical foundations as well as hands-on experience with verification/synthesis tools and SAT/SMT solvers. Students are expected to have completed undergraduate coursework in Foundations of Computer Science (CS 18200) or equivalent, Systems Programming (CS 25200) or equivalent, and Introduction to the Analysis of Algorithms (CS 38100) or equivalent. Mathematical maturity is expected.
Learning Outcomes1Express the expected behavior of programs in logic.
2Able to manually reason about satisfiability and validity of formulas in first-order logic (modulo theories).
3Use SAT/SMT solvers to check satisfiability and validity of formulas in first-order logic (modulo theories).
4Specify properties of programs using pre/postconditions, safety properties and assertions in first-order logic (modulo theories).
5Describe and apply core approaches for program verification.
6Explain and apply Hoare logic, invariant generation, abstract interpretation, abstraction-refinement, and bounded model checking.
7Ability to verify programs using tools such as Dafny and the Z3 SMT solver.
8Conduct original research in program synthesis.
9Explain and apply inductive synthesis and functional synthesis, different search techniques (enumerative, explicit, constraint-based), and some recent approaches based on machine learning.
10Choose and apply appropriate synthesis techniques to a problem domain of their choice.
11Ability to critically review and present current research in program synthesis.
Prerequisites
Restrictions
made by Purdue students.