menu

Lightweight Extraction of Syntactic Specifications

Taghdiri, Mana and Seater, Robert and Jackson, Daniel

PDF

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 values 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.


@inproceedings{taghdiri+:sigsoft06-lightweight-extraction,
  address = {New York, NY, USA},
  author = {Taghdiri, Mana and Seater, Robert and Jackson, Daniel},
  booktitle = {Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering},
  date-added = {2020-11-15 23:36:57 -0800},
  date-modified = {2020-11-15 23:36:57 -0800},
  isbn = {1595934685},
  keywords = {modular abstraction, syntactic specification, symbolic execution, symbolic summary},
  location = {Portland, Oregon, USA},
  numpages = {11},
  pages = {276--286},
  publisher = {Association for Computing Machinery},
  series = {SIGSOFT '06/FSE-14},
  title = {Lightweight Extraction of Syntactic Specifications},
  year = {2006},
  bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA2cGFwZXJzL3RhZ2hkaXJpK3NpZ3NvZnQwNi1saWdodHdlaWdodC1leHRyYWN0aW9uLWEucGRmTxEB5AAAAAAB5AACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////H3RhZ2hkaXJpK3NpZ3NvZnQwNiNGRkZGRkZGRi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAQADAAAKIGN1AAAAAAAAAAAAAAAAAAZwYXBlcnMAAgBVLzpVc2VyczpnYW1ibGluMjpzcmM6YnVpbGQtYmliOnBhcGVyczp0YWdoZGlyaStzaWdzb2Z0MDYtbGlnaHR3ZWlnaHQtZXh0cmFjdGlvbi1hLnBkZgAADgBgAC8AdABhAGcAaABkAGkAcgBpACsAcwBpAGcAcwBvAGYAdAAwADYALQBsAGkAZwBoAHQAdwBlAGkAZwBoAHQALQBlAHgAdAByAGEAYwB0AGkAbwBuAC0AYQAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAU1VzZXJzL2dhbWJsaW4yL3NyYy9idWlsZC1iaWIvcGFwZXJzL3RhZ2hkaXJpK3NpZ3NvZnQwNi1saWdodHdlaWdodC1leHRyYWN0aW9uLWEucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJABdAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAkU=},
  bdsk-url-1 = {https://doi.org/10.1145/1181775.1181809}
}
Top