| |
Jan 02, 2026
|
|
|
|
|
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.Credits: 3.00
Add to Portfolio (opens a new window)
|
|
