PROGRAM VERIFICATION AND SYNTHESIS
Formal methods for program verification. Model-checking techniques; linear temporal logic; computational tree logic; logic/automata connection; bisimulations; probabilistic model-checking. Special topics include: program synthesis, verification and synthesis of privacy properties. Knowledge of programming languages and compiler design strongly encouraged, such as COMP SCI 536 .
Topics
- program synthesis
- verification and synthesis of privacy properties
Topics explicitly listed in official catalogue description
Prerequisites & course information
Requisites: Graduate/professional standing Course Designation: Grad 50% - Counts toward 50% graduate coursework requirement Repeatable for Credit: No Last Taught: Spring 2025 Learning Outcomes: 1. Logic: Syntax and formal semantics of temporal logics such as LTL and MSO and formalizing software safety properties. Translations from temporal logics to automata. Audience: Graduate 2. Model Checking: Understand algorithms for checking whether a program satisfies a temporal property in temporal logic and apply such algorithms to verification problems. Audience: Graduate 3. Synthesis: Understand and apply state-of-the-art program synthesis algorithms such as counterexample-guided inductive synthesis, syntax-guided synthesis, sketching, and MCMC sampling. Audience: Graduate Learning Outcomes: 1. Logic: Syntax and formal semantics of temporal logics such as LTL and MSO and formalizing software safety properties. Translations from temporal logics to automata. Audience: Graduate 2. Model Checking: Understand algorithms for checking whether a program satisfies a temporal property in temporal logic and apply such algorithms to verification problems. Audience: Graduate 3. Synthesis: Understand and apply state-of-the-art program synthesis algorithms such as counterexample-guided inductive synthesis, syntax-guided synthesis, sketching, and MCMC sampling. Audience: Graduate
Sources
- Course catalogue ↗2026-2027