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 JanDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00 | |||
10:30 30mTalk | Synthesizing Program-Specific Static Analyses Off the Beaten Track Colin Gordon Drexel University File Attached | ||
11:00 30mTalk | On quantifying the degree of unsoundness of static analyses Off the Beaten Track Dimitrios Vardoulakis Google File Attached | ||
11:30 30mTalk | Explaining Type Errors Off the Beaten Track Brent Yorgey Hendrix College, Richard A. Eisenberg Bryn Mawr College, USA, Harley D. Eades III Augusta University File Attached |