Computer-Aided Verification

3 credits · Graduate

Introduction to the theory and practice of formal methods for the design and analysis of systems, with a focus on automated algorithmic techniques. Covers selected topics in computational logic and automata theory including formal models of reactive systems, temporal logic, model checking, and automated theorem proving. Applications in hardware and software verification, analysis of embedded, real-time, and hybrid systems, computer security, synthesis, planning, constraint solving, and other areas will be explored as time permits.