96-770 Software Verification and Testing
In the first part of the course I will talk about symbolic execution and program testing. Symbolic execution is a systematic program analysis technique that has become increasingly popular in recent years, due to algorithmic advances and availability of computational power and constraint solving technology. I will review different flavors of symbolic execution, ranging from generalized symbolic execution to dynamic symbolic execution or concolic testing. I will also describe some challenges to symbolic execution, such as dealing with: looping constructs, multi-threading, recursive data structures, and complex mathematical constraints, as well as scalability challenges due to the path explosion problem. I will discuss some techniques and tools that address these challenges. Finally I will discuss the application of symbolic execution to software testing. If time permits, I will also review applications to: security, robustness, reliability and load testing.
Credit units: 12 (Summer)