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.