ECEN-5139 (3) Computer-Aided Verification

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 prereq., ECEN 2073 or CSCI 2824. Department enforced requisite., general proficiency in discrete mathematics and programming. Same as CSCI 5135. Requisites: Restricted to any graduate students or Electrical/Computer Engineering or Electrical Engineering Concurrent Degree majors only.