Synthesizing Program-Specific Static Analyses

Gordon, Colin S.

Off the Beaten Track Workshop (OBT'18), January 2018

pdf url arXiv

Abstract

Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of interest, and significant development resources. As a result, most program analyses target properties that are universally of interest (e.g., absence of null pointer dereference) or nearly so (e.g., deadlock freedom). However, many interesting program properties that would benefit from static checking are specific to individual programs, or sometimes programs utilizing a certain library. It is impractical to devote program analysis and verification experts to these problems. We propose instead to work on example-based synthesis of program analyses within well-understood domains like type qualifier systems and effect systems. The dynamic behaviors behind the classes of problems these systems prevent correspond to examples that developers who lack expertise in static analysis can readily provide (data flow paths, or stack traces).

Bibtex

@inproceedings{obt18,
  abbr = {OBT},
  author = { Gordon, Colin S. },
  title = {{Synthesizing Program-Specific Static Analyses}},
  bibtex_show = {true},
  booktitle = {{Off the Beaten Track Workshop (OBT'18)}},
  address = {{Los Angeles, CA, USA}},
  year = 2018,
  month = "January",
  pdf = {papers/obt18.pdf},
  arxiv = {1810.06600},
  slides = {papers/obt18_slides.pdf},
  url = {https://popl18.sigplan.org/event/obt-2018-synthesizing-program-specific-static-analyses},
  note = "Position paper.",
  abstract = {Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of interest, and significant development resources. As a result, most program analyses target properties that are universally of interest (e.g., absence of null pointer dereference) or nearly so (e.g., deadlock freedom). However, many interesting program properties that would benefit from static checking are specific to individual programs, or sometimes programs utilizing a certain library. It is impractical to devote program analysis and verification experts to these problems. We propose instead to work on example-based synthesis of program analyses within well-understood domains like type qualifier systems and effect systems. The dynamic behaviors behind the classes of problems these systems prevent correspond to examples that developers who lack expertise in static analysis can readily provide (data flow paths, or stack traces).}
}