Computer Science 357D Static Analysis of Programs and Reactive Systems  Spring 2007

• A Hierarchy of Numerical Abstract Domains: Polyhedra are the most popular abstract domain for numerical programs. They are usually sufficiently expressive to represent most properties of interest. Their main disadvantage, though, is their high complexity in terms of time and space. Therefore, abstract domains have been studied that are less expressive, but operations can be performed in polynomial time. Following are papers describing a range of such domains:
  • Patrick Cousot & Radhia Cousot. Static Determination of Dynamic Properties of Programs. In Proceedings of the second international symposium on Programming, B. Robinet (Ed), Paris, France, pages 106--130, april 13-15 1976, Dunod, Paris.
  • Antoine Mine, A New Numerical Abstract Domain Based on Difference-Bound Matrices in Program As Data Objects II, May 2001, LNCS 2053, pages 155-172
  • Antoine Mine, The Octagon Abstract Domain in Analysis, Slicing and Transformation, October 2001, IEEE, pages 310-319
  • Antoine Mine,, A Few Graph-Based Relational Numerical Abstract Domains, in Static Analysis Symposium, September 2002, LNCS 2477, pages 117-132
  • Antoine Mine, The Octagon Abstract Domain to appear in Higher-Order and Symbolic Computation, 2006 (long).
  • R. Clarisó and J. Cortadella, The octahedron abstract domain. In 11th Static Analysis Symposium (SAS'04), volume 3148 of Lecture Notes in Computer Science, pages 312-327. Springer-Verlag, August 2004.
  • Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Scalable Analysis of Linear Systems using Mathematical Programming In Proc.of Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, pp 21-47, Springer Verlag, 2005.
• Static analysis of executables: Thomas Reps et al have developed and implemented methods for the static analysis of executables.
  • Balakrishnan, G. and Reps, T., Analyzing memory accesses in x86 executables. In Proc. Int. Conf. on Compiler Construction, Springer-Verlag, New York, NY, 2004, 5-23.
  • Reps, T., Balakrishnan, G., and Lim, J., Intermediate-representation recovery from low-level code. In Proc. Workshop on Partial Evaluation and Program Manipulation (PEPM), (Charleston, SC, Jan. 9-10, 2006)
  • Xu, Z., Miller, B., and Reps, T., Safety checking of machine code. In SIGPLAN '00: Proceedings of the ACM Conference on Programming Language Design and Implementation, (Vancouver B.C., Canada, June 18-21, 2000), pp. 70-82.
  • Xavier Rival. Invariant Translation-Based Certification of Assembly Code. In International Journal on Software and Tools for Technology Transfer Springer Verlag, 2004.
• Acceleration techniques: Acceleration techniques attempt to approximate an infinite sequence of transitions by a meta transition to compute an approximation of the reachable state space in a finite number of steps.
  • A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Proc. 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS 2002), Kanpur, India, Dec. 2002, volume 2556 of Lecture Notes in Computer Science, pages 145-156. Springer, 2002.
  • S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Proc. 15th Int. Conf. Computer Aided Verification (CAV 2003), Boulder, CO, USA, July 2003, volume 2725 of Lecture Notes in Computer Science, pages 118-121. Springer, 2003.
  • S. Bardin, A. Finkel, and J. Leroux. FASTer acceleration of counter automata in practice. In Proc. 10th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), Barcelona, Spain, Apr. 2004, volume 2988 of Lecture Notes in Computer Science, pages 576-590. Springer, 2004.
  • J. Leroux, G. Sutre. Flat counter automata almost everywhere!. In Proc. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, Oct. 2005 , volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005.
  • J. Leroux. Complete Linear Acceleration for Convex Binary Relations . Labri Technical Report 1387-06, Feb. 20, 2006.
• Generation of nonlinear invariants:
  • Roberto Bagnara, Enric Rodríguez Carbonell and Enea Zaffanella, Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra, In Proceedings of the 12th International Symposium on Static Analysis (SAS'05) (London, UK, September 2005), vol. 3672 of Lecture Notes in Computer Science, C. Hankin and I. Silveroni, Eds., pp. 19-34.
  • Markus Müller-Olm and Helmut Seidl. Computing polynomial program invariants. Information Processing Letters (IPL) 91(5), pages 233-244, 2004.
  • Enric Rodríguez-Carbonell and Deepak Kapur. An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants, Springer-Verlag LNCS. In 11th Static Analysis Symposium 2004 (SAS'04), August 2004, Verona (Italy)
  • Patrick Cousot, Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (Invited paper). In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17\u201419, 2005. Lecture Notes in Computer Science 3385, © Springer, Berlin, pp. 1\u201424.
  • Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Non-Linear Loop Invariant Generation, In Principles of Programming Languages (POPL 2004).
• ASTREE project
• Any combination of Patrick Cousot's papers.
• Widening/Narrowing Operators
• Interprocedural Static Analysis
• Combining Abstract Interpreters and Join Algorithms
  • Sumit Gulwani, Ashish Tiwari and George Necula, Join Algorithms for the Theory of Uninterpreted Functions, In the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004)
  • Sumit Gulwani, Ashish Tiwari, Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions, ESOP 2006.
  • Sumit Gulwani, Ashish Tiwari, Combining Abstract Interpreters, to appear in PLDI 2006.