Go to Main Content

Purdue Self-Service



Catalog Entries


Fall 2023
Feb 21, 2024
Transparent Image
Information Select the Course Number to get further detail on the course. Select the desired Schedule Type to find available classes for the course. The Schedule Type links will be available only when the schedule of classes is available for the selected term.

CS 56000 - Reasoning About Programs
Credit Hours: 3.00. 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.
3.000 Credit hours

Syllabus Available
Levels: Graduate, Professional, Undergraduate
Schedule Types: Distance Learning, Lecture

Offered By: College of Science
Department: Computer Science

Course Attributes:
Upper Division

May be offered at any of the following campuses:     
      West Lafayette

Learning Outcomes: 1. Express the expected behavior of programs in logic. 2. Able to manually reason about satisfiability and validity of formulas in first-order logic (modulo theories). 3. Use SAT/SMT solvers to check satisfiability and validity of formulas in first-order logic (modulo theories). 4. Specify properties of programs using pre/postconditions, safety properties and assertions in first-order logic (modulo theories). 5. Describe and apply core approaches for program verification. 6. Explain and apply Hoare logic, invariant generation, abstract interpretation, abstraction-refinement, and bounded model checking. 7. Ability to verify programs using tools such as Dafny and the Z3 SMT solver. 8. Conduct original research in program synthesis. 9. Explain and apply inductive synthesis and functional synthesis, different search techniques (enumerative, explicit, constraint-based), and some recent approaches based on machine learning. 10. Choose and apply appropriate synthesis techniques to a problem domain of their choice. 11. Ability to critically review and present current research in program synthesis.

Return to Previous New Search XML Extract
Transparent Image
Skip to top of page