Current approaches combining multiple static analyses deriving different, independent properties focus either on modularity or performance.
Whereas declarative approaches facilitate modularity and automated, analysis-independent optimizations, imperative approaches foster manual, analysis-specific optimizations.
In this paper, we present a novel approach to static analyses that leverages the modularity of blackboard systems and combines declarative and imperative techniques.
Our approach allows exchangeability, and pluggable extension of analyses in order to improve sound(i)ness, precision, and scalability and explicitly enables the combination of otherwise incompatible analyses.
With our approach integrated in the OPAL framework, we were able to implement various dissimilar analyses, including a points-to analysis that outperforms an equivalent analysis from Doop, the state-of-the-art points-to analysis framework.
Thu 12 Nov Times are displayed in time zone: (UTC) Coordinated Universal Time change
|08:30 - 08:32|
|Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization|
Research PapersDOI Pre-print Media Attached
|08:33 - 08:34|
|Inherent Vacuity for GR(1) Specifications|
|08:35 - 08:36|
|Interval Counterexamples for Loop Invariant Learning|
|08:37 - 08:38|
|Modular Collaborative Program Analysis in OPAL|
Dominik HelmTU Darmstadt, Germany, Florian KüblerTU Darmstadt, Germany, Michael ReifTU Darmstadt, Germany, Michael EichbergTU Darmstadt, Germany, Mira MeziniTU Darmstadt, GermanyDOI
|08:39 - 08:40|
|Past-Sensitive Pointer Analysis for Symbolic Execution|
David TrabishTel Aviv University, Israel, Timotej KapusImperial College London, UK, Noam RinetzkyTel Aviv University, Cristian CadarImperial College London, UKDOI Pre-print Media Attached
|08:41 - 09:00|
|Conversations on Analysis 4|