Synthesizing Program-Specific Static Analyses
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).
Abstract (obt18-paper2.pdf) | 297KiB |
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
10:30 - 11:00 Talk | Synthesizing Program-Specific Static Analyses Off the Beaten Track Colin GordonDrexel University File Attached | ||
11:00 - 11:30 Talk | On quantifying the degree of unsoundness of static analyses Off the Beaten Track Dimitrios VardoulakisGoogle File Attached | ||
11:30 - 12:00 Talk | Explaining Type Errors Off the Beaten Track Brent YorgeyHendrix College, Richard A. EisenbergBryn Mawr College, USA, Harley D. Eades IIIAugusta University File Attached |