CIS 673: Computer-Aided Verification, Fall 2012
Class: Tues Thurs 10.30--12.00
Introduction
Over the past two decades, techniques for formal verification have matured
to allow analysis of real-world software.
This course will introduce students to methods and tools
for software verification.
During Fall 2012, we plan to cover following topics
- Program analysis: How to approximate queries about program variables using static dataflow analysis?
- Deductive verification: How to prove properties of programs?
- Software model checking: How to combine abstraction, symbolic search, and counter-example guided abstraction refinement
to automatically verify software?
- Constraint solvers: How can modern SAT and SMT solvers be used in software verification?
- Concurrency analysis: How to detect synchronization-related bugs in multi-threaded software?
- Software synthesis: How can software analysis be used to assist programmers during software development stage?
Prerequisites
The course requires basic knowledge of algorithms, data structures,
programming languages, automata theory, computational complexity, and
propositional logic.
The course requires mathematical maturity, and is appropriate
for graduate students who wish to pursue research in
formal methods, software analysis, or related areas.
If you need more information to decide, contact the instructor.
Last updated on March 26, 2012 by Rajeev Alur