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 NovDisplayed time zone: (UTC) Coordinated Universal Time change
08:30 - 09:00
|Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization|
Research PapersDOI Pre-print Media Attached
|Inherent Vacuity for GR(1) Specifications|
|Interval Counterexamples for Loop Invariant Learning|
|Modular Collaborative Program Analysis in OPAL|
Dominik Helm TU Darmstadt, Germany, Florian Kübler TU Darmstadt, Germany, Michael Reif TU Darmstadt, Germany, Michael Eichberg TU Darmstadt, Germany, Mira Mezini TU Darmstadt, GermanyDOI
|Past-Sensitive Pointer Analysis for Symbolic Execution|
David Trabish Tel Aviv University, Israel, Timotej Kapus Imperial College London, UK, Noam Rinetzky Tel Aviv University, Cristian Cadar Imperial College London, UKDOI Pre-print Media Attached
|Conversations on Analysis 4|