Go to Main Content

Purdue Self-Service



Syllabus Information


Fall 2023
Jun 15, 2024
Transparent Image
Information Use this page to maintain syllabus information, learning objectives, required materials, and technical requirements for the course.

Syllabus Information
CS 56000 - Reasoning About Programs
Associated Term: Fall 2023
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.
Required Materials:
Technical Requirements:

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