Automated Verification

Prerequisite: Computer Science 130A-B and 138.
Covers automated verification algorithms and tools. Topics include: temporal logics, fixpoint characterizations of temporal properties, model checking, symbolic verification, explicit-state verification, verification using automated theorem provers, automated abstraction.