 | 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. Typically offered Fall.
3.000 Credit hours Syllabus Available Levels: Undergraduate, Graduate, Professional 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. |
 |