Regularly annotated set constraints

ABSTRACT

A general class of program analyses area combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.

REFERENCES

• 1: Alexander Aiken , Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su, A Toolkit for Constructing Type- and Constraint-Based Program Analyses, Proceedings of the Second International Workshop on Types in Compilation, p.78-96, March 25-27, 1998
• 2: Alexander Aiken , Dexter Kozen , Moshe Y. Vardi , Edward L. Wimmers, The Complexity of Set Constraints, Selected Papers from the 7th Workshop on Computer Science Logic, p.1-17, September 13-17, 1993
• 3: Rajeev Alur , P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, June 13-16, 2004, Chicago, IL, USA [doi>10.1145/1007352.1007390]
• 4: H. Chen, D. Dean, and D. Wagner. Model checking one million lines of C code. In Proc. of the 11th Annual Network and Distributed System Security Symp., pages 171--185, Feb4-6, 2004.
• 5: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 6: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 7: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 8: M. Fähndrich, J. Rehof, and M. Das. From polymorphic subtyping to cfl reachability: Context-sensitive flow analysis using instantiation constraints. Technical Report MSR-TR-99-84, Microsoft Research, 1999.
• 9: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C, Proceedings of the 7th International Symposium on Static Analysis, p.175-198, June 29-July 01, 2000
• 10: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 11: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.254-263, June 2001, Snowbird, Utah, United States
• 12: Susan Horwitz , Thomas Reps , Mooly Sagiv, Demand interprocedural dataflow analysis, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.104-115, October 12-15, 1995, Washington, D.C., United States
• 13: T. Jensen, D. L. Metayer, and T. Thorn. Verification of control flow based security properties. In Proc. of the 1999 IEEE Symp. on security and Privacy, 1999.
• 14: J. Kodumal. Banshee: A toolkit for constructing constraint-based analyses. http://banshee.sourceforge.net, 2005.
• 15: John Kodumal , Alex Aiken, The set constraint/CFL reachability connection in practice, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 16: J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In Proc. of the 12th International Static Analysis Symposium, pages 218--234, Sept. 2005.
• 17: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 18: Yanhong A. Liu , Tom Rothamel , Fuxiang Yu , Scott D. Stoller , Nanjun Hu, Parametric regular path queries, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 19: Ana Milanova , Barbara G. Ryder, Annotated Inclusion Constraints for Precise Flow Analysis, Proceedings of the 21st IEEE International Conference on Software Maintenance (ICSM'05), p.187-196, September 25-30, 2005 [doi>10.1109/ICSM.2005.24]
• 20: Jens Palsberg, Efficient inference of object types, Information and Computation, v.123 n.2, p.198-209, Dec. 1995 [doi>10.1006/inco.1995.1168]
• 21: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 22: Thomas Reps, Undecidability of context-sensitive data-independence analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.162-186, Jan. 2000 [doi>10.1145/345099.345137]
• 23: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 24: T. Reps, S. Schwoon, and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proc. 10th Int. Static Analysis Symp., pages 189--213, 2003.
• 25: Atanas Rountev , Ana Milanova , Barbara G. Ryder, Points-to analysis for Java using annotated constraints, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.43-55, October 14-18, 2001, Tampa Bay, FL, USA
• 26: Manu Sridharan , Denis Gopan , Lexin Shan , Rastislav Bodík, Demand-driven points-to analysis for Java, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 27: Zhendong Su , Manuel Fähndrich , Alexander Aiken, Projection merging: reducing redundancies in inclusion constraint graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-95, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325706]
• 28: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Algorithms, Design, Experimentation, Languages, Theory

Keywords:
annotated inclusion constraints, context-free language reachability, flow analysis, pushdown model checking, set constraints