Covers theoretical and practical aspects of verification of finite-state systems (hardware) and infinite-state systems (programs). Model checking: temporal logics, explicit-state and symbolic search, BDDs. Constraint solvers: SAT solvers, decision procedures. Program verification: invariants, partial vs. total correctness, abstraction. Recommended prerequisite: CSCI 2824. Department enforced requisite: general proficiency in discrete mathematics and programming. Same as CSCI 5135.
instructor(s)
Somenzi, Fabio
Primary Instructor
- Fall 2019 / Fall 2020 / Fall 2021 / Fall 2022 / Fall 2023 / Fall 2024
