CS 639: Program Analysis, Verification and Testing

Prerequisites

Discrete Mathematics (CS 201), Data Structures and Algorithms (CS 210), Theory of Computation (CS 340)

Course Contents

The long yearned dream of establishing the correctness of programs has cata-pulted program analysis, verification and testing into the league of the one of the most exciting research areas. This course aims to impart the students a grasp of the theoretical fundamentals of the subject; alongside, it also intends to provide them a purview of the practise via the study of some of the modern verification and testing tools.

 

Following is the outline of the proposed course:

1. Dataflow Analysis;
2. Interprocedural Analysis: functional, call-string and graph reachability based approaches
3. Abstract Interpretation;
4. Weakest Precondition, Floyd-Hoare Logic, Separation Logic;
5. SoftwareModel Checking: symbolic execution, state-space reduction, state-less model checking, counter-example guided abstraction refinement, model checking of concurrent programs
6. Program Testing: program testing basics, automatic test-case generation, directed testing.

 

Books and References

1. Edsger Wybe Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1997.
2. David Gries. The Science of Programming. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1987.
3. S. S. Muchnick and N. D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall: Englewood Cliffs, NJ, 1981.
4. Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Pro-gram Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999.
5. Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2006.
6. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA, 2004.
7. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model check-ing. MIT Press, Cambridge, MA, USA, 1999.
8. Glenford J. Myers. Art of Software Testing. John Wiley & Sons, Inc., New York, NY, USA, 1979.
9. Cem Kaner, Hung Q. Nguyen, and Jack L. Falk. Testing Computer Software. John Wiley & Sons, Inc., New York, NY, USA, 1993.
10. Relevant Research Papers.