An overview of the saturn project

ABSTRACT

We present an overview of the Saturn program analysis system, including a rationale for three major design decisions: the use of function-at-a-time, or summary-based, analysis, the use of constraints, and the use of a logic programming language to express program analysis algorithms. We argue that the combination of summaries and constraints allows Saturn to achieve both great scalability and great precision, while the use of a logic programming language with constraints allows for succinct, high-level expression of program analyses.

REFERENCES

• 1: A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and P. Hawkins. The Saturn program analysis system. http://saturn.stanford. edu, 2006.
• 2: Francois Bancilhon , David Maier , Yehoshua Sagiv , Jeffrey D Ullman, Magic sets and other strange ways to implement logic programs (extended abstract), Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.1-15, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15399]
• 3: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 4: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, pages 168--176. Springer, 2004.
• 5: Roger F. Crew, ASTLOG: a language for examining abstract syntax trees, Proceedings of the Conference on Domain-Specific Languages on Conference on Domain-Specific Languages (DSL), 1997, p.18-18, October 15-17, 1997, Santa Barbara, California
• 6: Isil Dillig , Thomas Dillig , Alex Aiken, Static error detection using semantic inconsistency inference, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 7: 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
• 8: Brian Hackett , Alex Aiken, How is aliasing used in systems software?, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181785]
• 9: Brian Hackett , Manuvir Das , Daniel Wang , Zhe Yang, Modular checking for buffer overflows in the large, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134319]
• 10: 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
• 11: J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In Proceedings of the 12th International Static Analysis Symposium, pages 218--234. London, United Kingdom, September 2005.
• 12: Monica S. Lam , John Whaley , V. Benjamin Livshits , Michael C. Martin , Dzintars Avots , Michael Carbin , Christopher Unkel, Context-sensitive program analysis as database queries, Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 13-15, 2005, Baltimore, Maryland [doi>10.1145/1065167.1065169]
• 13: V. Benjamin Livshits , Monica S. Lam, Tracking pointers with path and context sensitivity for bug detection in C programs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 14: R. Milner. A theory of type polymorphism in programming languages. Journal of Computer and System Sciences, 1998.
• 15: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 16: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type inference, Conference proceedings on Object-oriented programming systems, languages, and applications, p.146-161, October 06-11, 1991, Phoenix, Arizona, United States
• 17: T. Reps. Demand interprocedural program analysis using logic databases. In Applications of Logic Databases, pages 163--196, 1994.
• 18: Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. JLP, 29(1-3):17--64, 1996.
• 19: J.D. Ullman. Principles of Database and Knowledge-Base Systems. Computer Science Press, 1989.
• 20: Yichen Xie , Alex Aiken, Context- and path-sensitive memory leak detection, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 21: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA

INDEX TERMS

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

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

General Terms:
Design, Experimentation, Languages

Keywords:
boolean satisfiability, program analysis, verification