Automated Software Analysis Group

Lightweight Extraction of Syntactic Specifications

  • Author:

    Mana Taghdiri, Robert Seater, Daniel Jackson

  • Place:

    International Symposium on Foundations of Software Engineering (FSE), 2006

  • Date: Nov. 2006
  • A method for extracting syntactic specifications from heap-manipulating code is described. The state of the heap is represented as an environment mapping each variable or field to a relational expression. A procedure is executed symbolically, obtaining an environment for the post-state that gives the value of each variable and field in terms of the val- ues of variables and fields of the pre-state. Approximation is introduced by forming relational unions at merge points in the control flow graph, and by widening union-of-join expressions to transitive closures. The resulting analysis is linear in the length of the code and the number of fields, but capable of producing non-trivial specifications of surprising accuracy.

BibTex

@InProceedings{taghdiri-etal-2006,
    author    = "M. Taghdiri and R. Seater and D. Jackson",
    title     = {Lightweight Extraction of Syntactic Specifications},
    booktitle = {14th International Symposium on Foundations of Software Engineering (FSE)},
    pages     = {276-286},
    year      = {2006}
}