CS 598: Software Verification
3:30pm-4:45pm, Tuesdays and Thursdays
1131 Siebel Center
Scientific methods for engineering reliable software is a grand challenge in computer science. This course is dedicated to studying state-of-the-art techniques for ensuring high reliability of software. We will study several techniques, ranging from testing, type-checking, static analysis, and formal verification, for ensuing correctness to ensure safety and security.
The course will be driven by extensive student presentations of research papers and projects aimed to learn, explore, and perhaps even accomplish new research. The course will involve a project, aligned with the student's research area if possible. Graduate students already working on verification, security, or programming languages, with some basic knowledge of formal methods in verification, are encouraged to attend.
will differ from CS476 as we will not be using rewriting techniques,
and from CS477 as it will be more in-depth and research-oriented.
|Homework Number||Date posted||Date due||Homework handout||Homework LaTex Source|
|1||09/28||10/07||Homework #1||LaTeX source|
|Lec Num||Date||Material covered||Slide capture|
|2||Aug 26|| Floyd-Hoare verification technique:
Inductive invariants, strongest post, weakest pre
|3||Aug 31|| Floyd-Hoare verification:
|4||Sep 2|| Demo of Boogie, by Rajesh Karmani.
Brief introduction to logic
FOL, quantifier-free, Godel's theorems, theories.
|5||Sep 7|| Symbolic testing:
Path constraints, PEX tool and demo
|6,7||Sep 9, Sep 14|| Abstract Interpretation
General definition; Galois connections;
static analysis examples (reaching def, constant prop.)
numerical domains: intervals, octagons, polyhedra
|8||Sep 16||Widenings and Narrowings||Slides#8|
|9, 10||Sep 21, Sep 23|| Predicate Abstraction
Graf-Saidi approach, Cartesian abstraction
Counter-example guided abstraction refinement; Das-Dill technique
SLAM examples; ddverify examples and demo
|12||Sep 28|| Model Checking
Pushdown system model-checking
|13||Sep 30||Boolean decision diagrams and symbolic model-checking||Slides#13|