Committee

  • Zak Kincaid (advisor)
  • David Walker
  • Aarti Gupta

Title

Procedure Summarization via Vector Addition Systems and Inductive Linear Bounds. Slides

Abstract

All non-trivial questions concerning program dynamics are undecidable, so program analyzers often turn to heuristics to enable automated verification; these heuristics can cause analyzer behavior to be unpredictable, with slight changes to the input program radically changing the strength of the analysis. In this talk, I will present a procedure summarization technique that is monotone, guaranteeing a degree of predictability in the behavior of the analysis. We abstract programs as labeled rational vector addition systems with resets (VASR), which map each edge of the control flow graph to a VASR transformation. We show how to compute a VASR that is a best abstraction of a program expressed in linear arithmetic. We then show that the reachability relation of a VASR constrained to sequences of labels in a context free language is computable and leverage this to compute a logical summary of the executions of a VASR over paths through the input program. Finally, we describe a refinement which synthesizes potential functions bounding the number of calls to each procedure and prunes the language of paths through our program which we consider to those meeting the associated constraints. Together, these techniques combine for a summarization procedure which is performant, powerful, and predictable.

Reading List

Papers

  1. "Compositional Certified Resource Bounds". Quentin Carbonneaux, Jan Hoffman, and Zhong Shao (2015). (link)
  2. "Context-Free Commutative Grammars with Integer Counters and Resets". Dmitry Chistikov, Christoph Haase, Simon Halfon (2018). (link)
  3. "Loop Summarization with Rational Vector Addition Systems". Jake Silverman and Zachary Kincaid (2019). (link)
  4. "On the Complexity of Equational Horn Clauses". Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick (2005). (link)
  5. "Algebraic Program Analysis". Zachary Kincaid, Thomas Reps, and John Cyphert (2021). (link)
  6. "Software Model Checking". Ranjit Jhala and Rupak Makumdar (2009). (link)
  7. "Precise Interprocedural Dataflow Analysis via Graph Reachability". Thomas Reps, Susan Horwitz, Mooly Sagiv (1995). (link)
  8. "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints". Patrick Cousot, Radhia Cousot (1977). (link)
  9. "Symbolic Register Automata". Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva . (link)
  10. "Bebop: A Symbolic Model Checker for Boolean Programs". Thomas Ball and Sriram Rajamani. (link)

Textbooks

  1. Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007.
  2. Anders Moller and Michael Schwartzbach. Static Program Analysis. Arhaus University, 2023.

Questions

  1. [Dave] What is predicate abstraction? Run through the process of boolean program abstraction of the following program beginning with just an abstraction of the state of the lock. What would the counterexample be? Show how the abstraction would be refined. Does this abstraction refinement always terminate?
    lock x; int y = 17;
    assert(unlocked(x));
    if (y > 0) {
    lock(x);
    }
    if (y > 0) {
    release(x);
    }
    assert(unlocked(x));
  2. [Aarti]: Describe some algorithmic approaches to abstraction refinement. How would an algorithm automatically synthesize a boolean for (y > 0)? Describe how Bebop would model check the boolean program you wrote down. How does Bebop summarize procedures?
  3. [Zak] What is a Galois connection and what is its connection to abstract interpretation? Are there any useful numerical abstract domains to which we do not have a Galois connection? What is the connection between your work and abstract interpretation?