 | Use this page to maintain syllabus information, learning objectives, required materials, and technical requirements for the course. |
| CS 56000 - Reasoning About Programs |
|---|
|
Associated Term:
Fall 2019
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 |
 |