Comparing Transparent Static Analyzers with Open Verification Dashboard
This program is tentative and subject to change.
Given an input program, sound static analyzers compute a list of \emph{potential} runtime errors in it. Static analysis practitioners have difficulties measuring the precision of static analyzers and comparing their results. In this work, we formalize a notion of \emph{transparent static analyzers} providing a fine-grained output of the \emph{proof obligations they verified}. This transparent output enables a semantics-directed, fine-grained comparison and the combination of static analyzers. We introduce the Open Verification Dashboard (OVD), which provides a unified interface to aggregate the results of multiple static analyzers. By juxtaposing verified properties and outstanding warnings, OVD highlights coverage gaps, variabilities and inconsistencies across tools. We experimentally evaluate the benefits of OVD on benchmarks from the Competition on Software Verification (SV-COMP). This work paves the way for a static analysis standard for C runtime error reporting.
This program is tentative and subject to change.
Fri 3 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 22mTalk | Scaling Bottom-up IFDS Taint Analysis with Optimized Data-flow Encoding Technical Papers | ||
11:22 22mTalk | DelExp: a Relational Container Abstraction with Applications to Compositional Analysis Technical Papers Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université | ||
11:45 22mTalk | Comparing Transparent Static Analyzers with Open Verification Dashboard Technical Papers Tom Goalard University of Rennes, Karoliine Holter University of Tartu, Estonia, Simmo Saan University of Tartu, Estonia, Vesal Vojdani University of Tartu, Raphaël Monat Inria and University of Lille | ||
12:07 22mTalk | Field-Sensitive Over-Tainting Reduction in IFDS Taint Analysis via CFL-Reachability Technical Papers | ||