Exercises & Recommended Readings
for “HighQuality Scalable Checking using Modular PathSensitive Analysis”
Exercises: 
[PathSensitive Loop Widening] Work out the mathematical detail of pathsensitive loop widening. Prove that the algorithm terminates.

[Theorem Proving] Using the observation that linear combination with small integer coefficients would suffice most of the time for developers’ reasoning, construct a theorem prover for linear inequality constraints based on graph search. A good starting point is the reduction of solving difference constraints to the shortestpath problem (Cormen, et al. 2001). How would you add the reasoning power for modular arithmetic?

[Defect Presentation] A pathsensitive analysis uses sharing to achieve coverage while ensuring termination and maintaining a reasonable cost. But when you want to show a potential issue to a developer, it is best to show them the symbolic information along code paths. For one defect found, there could be infinite number of paths leading to the defects, due to the presence of loops. How would you present the set of infinite paths to the developers in an understandable manner?
If you feel like, you can send your solutions, comments, or questions to me (zhe.yang@microsoft.com).
On Buffer Access Checking
(Dor, Rodeh and Sagiv 2003): Assertassume framework for bufferaccess checking.
(Cousot and Halbwachs 1978): Original paper on the lattice of polyhedral and its application to find linear constraints in a program.
(Hackett, et al. 2006): Our work on buffer access checking. This article offers an overview of the workflow in use at Microsoft, the annotation language, the inference algorithm of the annotations, as well as a highlevel sketch of the pathsensitive checker.
General Introduction to Program Analysis and Domain Theory
(Schwartzbach n.d.): An efficient introduction to the techniques of program analysis.
(Nielson, Nielson and Hankin 1999): Standard textbook on program analysis.
(Winskel 1993): Chapter 8 offers a good introduction to domain theory
PathSensitive Dataflow Analysis
(Reps, Horwitz and Sagiv 1995): Seminar work on scalable interprocedural analysis. The simplest form of path sensitive analysis can be understood as graph reachability.
(Das, Lerner and Seigle 2002): Original paper on ESP shows a more sophisticated form of pathsensitive analysis, with applications to defect detection.
Theorem Provers (aka Decision Procedures)
(Cormen, et al. 2001): In this good old text book, you can find how to build a theorem prover for the simplest form of linear constraintsdifference constraintsusing a shortestpath algorithm.
(Shankar 2002): A nice survey paper on automated reasoning, and, in particular, on combining theorem provers.
(Nelson and Oppen 1979): Standard framework for combining decision procedures.
(Tarjan 1974): The standard algorithm for loop decomposition. A few articles in the last decades studies algorithms for dealing with irreducible flow graphs.
References
Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 2nd Edition. MIT Press, 2001.
Cousot, Patrick, and Nicolas Halbwachs. "Automatic Discovery of Linear Restraints Among Variables of a Program." Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL). Tucson, Arizona: ACM, 1978. 8496.
Das, Manuvir, Sorin Lerner, and Mark Seigle. "ESP: PathSensitive Program Verification in Polynomial Time." Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Berlin, Germany: ACM, 2002. 5768.
Dor, Nurit, Michael Rodeh, and Shmuel Sagiv. "CSSV: towards a realistic tool for statically detecting all buffer overflows in C." Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI). San Diego, California: ACM, 2003. 155167.
Hackett, Brian, Manuvir Das, Daniel Wang, and Zhe Yang. "Modular checking for buffer overflows in the large." 28th International Conference on Software Engineering (ICSE 2006). Shanghai, China: ACM, 2006. 232241.
Nelson, Greg, and Derek C. Oppen. "Simplification by Cooperating Decision Procedures." ACM Transactions on Programming Languages and Systems 1, no. 2 (1979): 245257.
Nielson, Flemming, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer, 1999.
Reps, Thomas W., Susan Horwitz, and Shmuel Sagiv. "Precise Interprocedural Dataflow Analysis via Graph Reachability." 22nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. San Francisco, California: ACM, 1995. 4961.
Schwartzbach, Michael I. "Lecture Notes on Static Analysis." http://www.brics.dk/~mis/static.pdf (accessed 2007).
Shankar, Natarajan. "Little Engines of Proof." FME 2002: Formal Methods  Getting IT Right, International Symposium of Formal Methods Europe (LICS 2391). Copenhagen, Denmark: Springer, 2002. 120.
Tarjan, Robert Endre. "Testing Flow Graph Reducibility." Journal of Computer and System Sciences (JCSS) 9, no. 3 (1974): 355365.
Winskel, Glynn. The Formal Semantics of Programming Languages. MIT Press, 1993. 