Sound and Reusable Components for Abstract Interpretation
Abstract interpretation is a methodology for defining sound static analyses. Yet, creating a new static analyzer is a laborious and difficult task, because the analyzer is often implemented from scratch and proven sound a posteriori. To address this problem, we propose a novel approach to construct abstract interpreters from reusable analyses components. Each analysis component captures a separate aspect of the analyzed language (stores, environments, exceptions, etc.). Furthermore, analysis components can be proven sound a priori and their soundness proof remains valid when composing components. We developed a framework for reusable analysis components in Haskell for arrow-based abstract interpreters and realized 10 sound and reusable analysis components. We (re)used these components to define a $k$-CFA analysis for PCF and a reaching definition analysis for a While language.
Thu 22 Nov
|10:00 - 10:25|
|10:25 - 10:50|
|10:50 - 11:15|
Trevor L. McDonellUtrecht University
|11:15 - 11:40|