(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 high-level sketch of the path-sensitive checker.

(Nielson, Nielson and Hankin 1999): Standard textbook on program analysis.

(Das, Lerner and Seigle 2002): Original paper on ESP shows a more sophisticated form of path-sensitive 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 constraints---difference constraints---using a shortest-path 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. 84-96.

Das, Manuvir, Sorin Lerner, and Mark Seigle. "ESP: Path-Sensitive Program Verification in Polynomial Time." *Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).* Berlin, Germany: ACM, 2002. 57-68.

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. 155-167.

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. 232-241.

Nelson, Greg, and Derek C. Oppen. "Simplification by Cooperating Decision Procedures." *ACM Transactions on Programming Languages and Systems* 1, no. 2 (1979): 245-257.

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 SIGPLAN-SIGACT Symposium on Principles of Programming Languages.* San Francisco, California: ACM, 1995. 49-61.

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. 1-20.

Tarjan, Robert Endre. "Testing Flow Graph Reducibility." *Journal of Computer and System Sciences (JCSS)* 9, no. 3 (1974): 355-365.

Winskel, Glynn. *The Formal Semantics of Programming Languages.* MIT Press, 1993.

**Share with your friends:**