Citation
Yamini Kannan, Koushik Sen. "Universal symbolic execution and its application to likely data structure invariant generation". Proceedings of the 2008 international symposium on Software testing and analysis, International Symposium on Software Testing and Analysis, 283-294, July, 2008.

Abstract
Local data structure invariants are asserted over a bounded fragment of a data structure around a distinguished node M of the data structure. An example of such an invariant for a sorted doubly linked list is "for all nodes M of the list, if M ≠ null and M.next ≠ null, then M.next.prev = M and M.value ≤ M.next.value." It has been shown that such local invariants are both natural and sufficient for describing a large class of data structures. This paper explores a novel technique, called Krystal, to infer likely local data structure invariants using a variant of symbolic execution, called universal symbolic execution. Universal symbolic execution is like traditional symbolic execution except the fact that we create a fresh symbolic variable for every read of a lvalue that has no mapping in the symbolic state rather than creating a symbolic variable only for inputs. This helps universal symbolic execution to symbolically track data flow for all memory locations along an execution even if input values do not flow directly into those memory locations. We have implemented our algorithm and applied it to several data structure implementations in Java. Our experimental results show that we can infer many interesting local invariants for these data structures.

Electronic downloads

• http://doi.acm.org/10.1145/1390630.1390665

• HTML

  Yamini Kannan, Koushik Sen. <a
  href="http://chess.eecs.berkeley.edu/pubs/506.html"
  >Universal symbolic execution and its application to
  likely data structure invariant generation</a>,
  Proceedings of the 2008 international symposium on Software
  testing and analysis, International Symposium on Software
  Testing and Analysis, 283-294, July, 2008.

• Plain text

  Yamini Kannan, Koushik Sen. "Universal symbolic
  execution and its application to likely data structure
  invariant generation". Proceedings of the 2008
  international symposium on Software testing and analysis,
  International Symposium on Software Testing and Analysis,
  283-294, July, 2008.

• BibTeX

  @inproceedings{KannanSen08_UniversalSymbolicExecutionItsApplicationToLikelyData,
      author = {Yamini Kannan and Koushik Sen},
      title = {Universal symbolic execution and its application
                to likely data structure invariant generation},
      booktitle = {Proceedings of the 2008 international symposium on
                Software testing and analysis},
      organization = {International Symposium on Software Testing and
                Analysis},
      pages = {283-294},
      month = {July},
      year = {2008},
      abstract = {Local data structure invariants are asserted over
                a bounded fragment of a data structure around a
                distinguished node M of the data structure. An
                example of such an invariant for a sorted doubly
                linked list is "for all nodes M of the list, if M
                ≠ null and M.next ≠ null, then M.next.prev = M
                and M.value ≤ M.next.value." It has been shown
                that such local invariants are both natural and
                sufficient for describing a large class of data
                structures. This paper explores a novel technique,
                called Krystal, to infer likely local data
                structure invariants using a variant of symbolic
                execution, called universal symbolic execution.
                Universal symbolic execution is like traditional
                symbolic execution except the fact that we create
                a fresh symbolic variable for every read of a
                lvalue that has no mapping in the symbolic state
                rather than creating a symbolic variable only for
                inputs. This helps universal symbolic execution to
                symbolically track data flow for all memory
                locations along an execution even if input values
                do not flow directly into those memory locations.
                We have implemented our algorithm and applied it
                to several data structure implementations in Java.
                Our experimental results show that we can infer
                many interesting local invariants for these data
                structures.},
      URL = {http://chess.eecs.berkeley.edu/pubs/506.html}
  }
  

Posted by Christopher Brooks on 18 Nov 2008.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.