High-Quality Scalable Checking using Modular Path-Sensitive Analysis

Download 9.48 Kb.

Date	09.01.2017
Size	9.48 Kb.
	#8639

Exercises & Recommended Readings
for “High-Quality Scalable Checking using Modular Path-Sensitive Analysis”

Exercises:

[Path-Sensitive Loop Widening] Work out the mathematical detail of path-sensitive 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 shortest-path problem (Cormen, et al. 2001). How would you add the reasoning power for modular arithmetic?
[Defect Presentation] A path-sensitive 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): Assert-assume framework for buffer-access 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 high-level sketch of the path-sensitive 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

Path-Sensitive Dataflow Analysis

(Reps, Horwitz and Sagiv 1995): Seminar work on scalable inter-procedural 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 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.

Identifying the loop nesting structure in a control-flow graph

(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.

Directory: research
research -> Charter School Enrollment Data Annual Report
research -> Lyra Viol Composers
research -> Geographies of Race and Food
research -> Author (s) title
research -> The Media and Intercollegiate Sports
research -> Project Title: Research and Development for goes-r risk Reduction Principal Investigator
research -> Why Everyday Life Matters: Class, Community and Making Life Livable Les Back
research -> Ecocritique and the Materialities of Animation

Download 9.48 Kb.

Share with your friends: