Go to Main Content

Purdue Self-Service



Detailed Course Information


Spring 2021
Jan 25, 2021
Transparent Image
Information Select the desired Level or Schedule Type to find available classes for the course.

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. Typically offered Fall.
3.000 Credit hours

Syllabus Available
Levels: Graduate, Professional, Undergraduate
Schedule Types: Distance Learning, Lecture
All Sections for this Course

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.

Must be enrolled in one of the following Programs:     
      Computer Science-PHD
      Computer Science-MS

GR CS 56000 Requisites

General Requirements:

Student Attribute: GR
May not be taken concurrently.  )
Course or Test: CS 18200
Minimum Grade of C
May not be taken concurrently.
Course or Test: CS 25200
Minimum Grade of C
May not be taken concurrently.
Course or Test: CS 38100
Minimum Grade of C
May not be taken concurrently. )

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