Document Open Access Logo

Comparing Transparent Static Analyzers with Open Verification Dashboard

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.8.pdf
  • Filesize: 1.25 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
  • Software and its engineering → Software testing and debugging
Keywords
  • automated static analysis
  • multi-tool integration
  • interoperability
  • proof obligations
  • result aggregation
  • verification progress
  • selectivity metric
  • reproducibility
  • dashboard

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ECOOP.2026.8

Author Details

Tom Goalard
  • ENS Rennes, Campus de Ker Lann, 11 avenue Robert Schuman, 35170 Bruz, France
Karoliine Holter
  • Institute of Computer Science, University of Tartu, Estonia
Simmo Saan
  • Institute of Computer Science, University of Tartu, Estonia
Vesal Vojdani
  • Institute of Computer Science, University of Tartu, Estonia
Raphaël Monat
  • Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL, 59000 Lille, France

Funding

This work is supported by the European Union and the Estonian Research Council via projects PRG2764 and TEM-TA119, by grant agreement ANR-24-CE25-7956-01 RAISIN from the French Agence Nationale de la Recherche, and by an Amazon Research Award, Fall 2024.

Supplementary Materials

References

  1. Esben Sparre Andreasen, Anders Møller, and Benjamin Barslev Nielsen. Systematic approaches for increasing soundness and precision of static analyzers. In Karim Ali and Cristina Cifuentes, editors, Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, SOAP@PLDI 2017, Barcelona, Spain, June 18, 2017, pages 31-36. ACM, 2017. URL: https://doi.org/10.1145/3088515.3088521.
  2. Pavel Avgustinov, Oege de Moor, Michael Peyton Jones, and Max Schäfer. QL: object-oriented queries on relational data. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming, ECOOP 2016, Rome, Italy, July 18-22, 2016, LIPIcs, pages 2:1-2:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.2.
  3. Paulína Ayaziová, Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl, and Jan Strejcek. Software verification witnesses 2.0. In Thomas Neele and Anton Wijs, editors, Model Checking Software - 30th International Symposium, SPIN 2024, Luxembourg City, Luxembourg, April 8-9, 2024, Proceedings, volume 14624 of Lecture Notes in Computer Science, pages 184-203. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-66149-5_11.
  4. Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Körner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, and Andreas Podelski. Ultimate automizer with a one-dimensional memory model - (competition contribution). In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, Lecture Notes in Computer Science, pages 589-594. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22749-2_37.
  5. Al Bessey, Ken Block, Benjamin Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles-Henri Gros, Asya Kamsky, Scott McPeak, and Dawson R. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53(2):66-75, 2010. URL: https://doi.org/10.1145/1646353.1646374.
  6. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Correctness witnesses: exchanging verification results between verifiers. In Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su, editors, Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, pages 326-337. ACM, 2016. URL: https://doi.org/10.1145/2950290.2950351.
  7. Dirk Beyer and Jan Strejcek. Improvements in software verification and witness validation: SV-COMP 2025. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), Part III, volume 15698 of Lecture Notes in Computer Science, pages 151-186. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90660-2_9.
  8. Dirk Beyer and Jan Strejcek. Evaluating software verifiers for C, Java, and SV-LIB - (report on SV-COMP 2026). In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, Lecture Notes in Computer Science, pages 461-502. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22749-2_23.
  9. Sandrine Blazy, David Bühler, and Boris Yakobowski. Structuring abstract interpreters through state and value abstractions. In Ahmed Bouajjani and David Monniaux, editors, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 112-130. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-52234-0_7.
  10. Guillaume Brat, Jorge A. Navas, Nija Shi, and Arnaud Venet. IKOS: A framework for static analysis based on abstract interpretation. In Dimitra Giannakopoulou and Gwen Salaün, editors, Software Engineering and Formal Methods - 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings, Lecture Notes in Computer Science, pages 271-277. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10431-7_20.
  11. Marco Campion, Caterina Urban, Mila Dalla Preda, and Roberto Giacobazzi. A formal framework to measure the incompleteness of abstract interpretations. In Manuel V. Hermenegildo and José F. Morales, editors, Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings, volume 14284 of Lecture Notes in Computer Science, pages 114-138. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44245-2_7.
  12. Yang Chen, Eric Eide, and John Regehr. csmith-project/creduce, 2025. original-date: 2012-02-28T15:55:07Z. URL: https://github.com/csmith-project/creduce.
  13. Maria Christakis and Christian Bird. What developers want and need from program analysis: an empirical study. In David Lo, Sven Apel, and Sarfraz Khurshid, editors, Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 332-343. ACM, 2016. URL: https://doi.org/10.1145/2970276.2970347.
  14. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Lecture Notes in Computer Science, pages 168-176. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_15.
  15. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C - A software analysis perspective. In George Eleftherakis, Mike Hinchey, and Mike Holcombe, editors, Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Lecture Notes in Computer Science, pages 233-247. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33826-7_16.
  16. Mark de Berg, Otfried Cheong, Marc van Kreveld, and Mark Overmars. Line Segment Intersection, pages 19-43. Springer, Berlin, Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-77974-2_2.
  17. Lisa Nguyen Quang Do, Stefan Krüger, Patrick Hill, Karim Ali, and Eric Bodden. Debugging static analysis. IEEE Trans. Software Eng., 46(7):697-709, 2020. URL: https://doi.org/10.1109/TSE.2018.2868349.
  18. ESLint Team and Nicholas C. Zakas. ESLint: The pluggable JavaScript linter. https://eslint.org/, 2025. Version 9.29.0, accessed 1 Jul 2025.
  19. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, pages 125-128. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_8.
  20. GitHub. Uploading static analysis results as SARIF to GitHub code scanning. https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github, 2025. GitHub Docs, accessed 1 Jul 2025.
  21. Tom Goalard. Open Verification Dashboard. Software, (visited on 2026-05-05). URL: https://github.com/sws-lab/open-verification-dashboard
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.25787
  22. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The SeaHorn verification framework. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, pages 343-361. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_20.
  23. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, pages 36-52. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_2.
  24. Karoliine Holter, Juhan Oskar Hennoste, Patrick Lam, Simmo Saan, and Vesal Vojdani. Abstract debuggers: Exploring program behaviors using static analysis results. In Jonathan Edwards and Marcel Taeumel, editors, Proceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2024, Pasadena, CA, USA, October 23-25, 2024, pages 130-146. ACM, 2024. URL: https://doi.org/10.1145/3689492.3690053.
  25. Gábor Horváth, Réka Kovács, Richárd Szalay, Zoltán Porkoláb, Gergely Orbán, and Dániel Krupp. Static code analysis with CodeChecker. CoRR, abs/2408.02220, 2024. URL: https://doi.org/10.48550/arXiv.2408.02220.
  26. Matthieu Journault, Antoine Miné, Raphaël Monat, and Abdelraouf Ouadjaout. Combinations of reusable abstract domains for a multilingual static analyzer. In Supratik Chakraborty and Jorge A. Navas, editors, Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers, Lecture Notes in Computer Science, pages 1-18. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-41600-3_1.
  27. Nat Karmios, Sacha-Élie Ayoun, and Philippa Gardner. Gillian debugging: Swinging through the (compositional symbolic execution) trees. In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, Lecture Notes in Computer Science, pages 195-214. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22749-2_10.
  28. Christian Klinger, Maria Christakis, and Valentin Wüstholz. Differentially testing soundness and precision of program analyzers. In Dongmei Zhang and Anders Møller, editors, Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, July 15-19, 2019, pages 239-250. ACM, 2019. URL: https://doi.org/10.1145/3293882.3330553.
  29. Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles. Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, Lecture Notes in Computer Science, pages 461-478, 2016. URL: https://doi.org/10.1007/978-3-319-47166-2_32.
  30. Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker - (competition contribution). In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Lecture Notes in Computer Science, pages 389-391. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_26.
  31. Woosuk Lee, Wonchan Lee, Dongok Kang, Kihong Heo, Hakjoo Oh, and Kwangkeun Yi. Sound non-statistical clustering of static analysis alarms. ACM Trans. Program. Lang. Syst., 39(4):16:1-16:35, 2017. URL: https://doi.org/10.1145/3095021.
  32. Martin Liška. marxin/cvise, 2025. original-date: 2020-04-18T13:04:05Z. URL: https://github.com/marxin/cvise.
  33. Microsoft SARIF Viewer Extension Team. SARIF viewer extension for Visual Studio Code. https://marketplace.visualstudio.com/items?itemName=MS-SarifVSCode.sarif-viewer, 2025. VS Code Marketplace listing, accessed 1 Jul 2025.
  34. Antoine Miné. Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang., 4(3-4):120-372, 2017. URL: https://doi.org/10.1561/2500000034.
  35. Mats Van Molle, Bram Vandenbogaerde, and Coen De Roover. Cross-level debugging for static analysers. In João Saraiva, Thomas Degueule, and Elizabeth Scott, editors, SLE, pages 138-148. ACM, 2023. URL: https://doi.org/10.1145/3623476.3623512.
  36. Anders Møller and Michael I. Schwartzbach. Static program analysis, June 2024. Department of Computer Science, Aarhus University, http://cs.au.dk/~amoeller/spa/. Google Scholar
  37. Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Mopsa-C: Modular domains and relational abstract interpretation for C programs (competition contribution). In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Part II, volume 13994 of Lecture Notes in Computer Science, pages 565-570. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_37.
  38. Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Easing maintenance of academic static analyzers. Int. J. Softw. Tools Technol. Transf., 26(6):673-686, 2024. URL: https://doi.org/10.1007/S10009-024-00770-1.
  39. Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. Mopsa-C with trace partitioning and autosuggestions (competition contribution). In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part III, Lecture Notes in Computer Science, pages 229-235. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90660-2_17.
  40. Tukaram Muske and Alexander Serebrenik. Survey of approaches for postprocessing of static analysis alarms. ACM Comput. Surv., 55(3):48:1-48:39, 2023. URL: https://doi.org/10.1145/3494521.
  41. OASIS. Static Analysis Results Interchange Format (SARIF) - Version 2.1.0, 2020. URL: https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html.
  42. John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. Test-case reduction for C compiler bugs. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, pages 335-346. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254104.
  43. Simmo Saan, Ali Rasim Kocal, Michael Petter, Karoliine Holter, Julian Erhard, Michael Schwarz, Vesal Vojdani, and Helmut Seidl. Goblint: A portfolio for mixed flow-sensitive abstract interpretation - (competition contribution). In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, Lecture Notes in Computer Science, pages 516-522. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22749-2_26.
  44. Simmo Saan, Michael Schwarz, Kalmer Apinis, Julian Erhard, Helmut Seidl, Ralf Vogler, and Vesal Vojdani. Goblint: Thread-modular abstract interpretation using side-effecting constraints - (competition contribution). In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Lecture Notes in Computer Science, pages 438-442. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_28.
  45. Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, and Vesal Vojdani. Correctness witness validation by abstract interpretation. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I, volume 14499 of Lecture Notes in Computer Science, pages 74-97. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-50524-9_4.
  46. Michael Schwarz and Julian Erhard. The digest framework: concurrency-sensitivity for abstract interpretation. Int. J. Softw. Tools Technol. Transf., 26(6):727-746, 2024. URL: https://doi.org/10.1007/S10009-024-00773-Y.
  47. Michael Schwarz and Julian Erhard. Data race detection by digest-driven abstract interpretation. In Yu-Fang Chen, Thomas P. Jensen, and Ondrej Lengál, editors, Verification, Model Checking, and Abstract Interpretation - 27th International Conference, VMCAI 2026, Rennes, France, January 12-13, 2026, Proceedings, Lecture Notes in Computer Science, pages 309-334. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-15700-3_15.
  48. Pascal Sotin. Quantifying the Precision of Numerical Abstract Domains. Research report, INRIA Grenoble Rhônes-Alpes, February 2010. URL: https://inria.hal.science/inria-00457324.
  49. Vesal Vojdani, Kalmer Apinis, Vootele Rõtov, Helmut Seidl, Varmo Vene, and Ralf Vogler. Static race detection for device drivers: the Goblint approach. In David Lo, Sven Apel, and Sarfraz Khurshid, editors, Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 391-402. ACM, 2016. URL: https://doi.org/10.1145/2970276.2970337.
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
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact