Search Results

Documents authored by Saan, Simmo


Document
Comparing Transparent Static Analyzers with Open Verification Dashboard

Authors: Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)


Abstract
Given an input program, sound static analyzers compute a list of potential runtime errors in it. However, measuring their precision and comparing their results remains challenging. In this work, we formalize a notion of transparent static analyzers that report the proof obligations they check, including both verified and unverified obligations. 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.

Cite as

Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 8:1-8:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{goalard_et_al:LIPIcs.ECOOP.2026.8,
  author =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  title =	{{Comparing Transparent Static Analyzers with Open Verification Dashboard}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{8:1--8:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.8},
  URN =		{urn:nbn:de:0030-drops-261049},
  doi =		{10.4230/LIPIcs.ECOOP.2026.8},
  annote =	{Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Document
Artifact
Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact)

Authors: Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)


Abstract
This artifact accompanies the eponymous article. It enables reproduction of the experimental claims made in the article that are covered by this description.

Cite as

Tom Goalard, Karoliine Holter, Simmo Saan, Vesal Vojdani, and Raphaël Monat. Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@Article{goalard_et_al:DARTS.12.1.6,
  author =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  title =	{{Comparing Transparent Static Analyzers with Open Verification Dashboard (Artifact)}},
  pages =	{6:1--6:15},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Goalard, Tom and Holter, Karoliine and Saan, Simmo and Vojdani, Vesal and Monat, Rapha\"{e}l},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.6},
  URN =		{urn:nbn:de:0030-drops-261430},
  doi =		{10.4230/DARTS.12.1.6},
  annote =	{Keywords: automated static analysis, multi-tool integration, interoperability, proof obligations, result aggregation, verification progress, selectivity metric, reproducibility, dashboard}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail