Go to Main Content

Purdue Self-Service

 

HELP | EXIT

Syllabus Information

 

Fall 2021
Mar 28, 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 2021
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
Release: 8.7.2.4