AnalyzeThat

AnalyzeThat'26, co-located with ETAPS!

Motivation

Static program analysis has matured to the point where many of our research tools can tackle substantial real-world code. What we lack are opportunities to exercise these tools on real software together, compare approaches, and learn from one another. Real-world audits require careful modeling and domain understanding, which can be time-consuming and scientifically unglamorous. AnalyzeThat creates a focused venue to make this work visible, collaborative and fun!

AnalyzeThat complements existing initiatives aimed at creating more robust and interchangeable verification tools. The Software-Verification Competition (SV-Comp) provides rigorous head-to-head evaluation on benchmarks with known outcomes established by human oracles. VerifyThis offers a two-day challenge to prove the correctness of intricate algorithms using deductive verification tools.

Goals

The aim of AnalyzeThat is to gather static analysis developers around a challenge: spending limited time auditing an open-source project. This event is built around two goals:

  • Open-ended exploration. There is no “ground truth” of bugs for the chosen project, the goal will be to prove some components of the project (un)safe. Each team will be free to choose the components they inspect, and their modeling of interactions.
  • Collaborative research. The event will foster sharing of practices when analyzing new projects, strengthen the community and offer opportunities for collaboration of researchers and tools. At the end of the workshop, we will have identified common struggles of participating tools, from which we can identify further research directions (identification of new challenging areas of application of static analysis; needs for developing novel abstractions)

What kind of open-source project? To gather a significant number of interested parties, this first event will target analysis of real-world, non-concurrent C programs/libraries. You can find example projects that could be considered here.

Calendar

  • 20 February 2026: Deadline to submit software to be considered for analysis, alongside note describing why it’s a real-world software which would be interesting to analyze.
  • 02 March 2026: Announcement of the chosen software to be analyzed until the workshop day
  • 10 March 2026: ETAPS early registration deadline
  • 12 April 2026: Workshop day @ ETAPS in Torino, dedicated to presenting obtained results, and discussing common issues.
    • Jörg Herter, Senior Tehnical Consultant for AbsInt, is invited speaker!

Join us on Zulip to participate!

Participating tools/teams (WIP)

NB: this list will be regularly updated. Contact us on Zulip to register!

Organizers

Schedule (tentative)

  • 8:55 – Welcome from the organizers
  • 9:00 – Keynote by Jörg Herter, Senior Tehnical Consultant for AbsInt
    "Sound Static Analysis at Scale: Practical Lessons from Industry" This talk shares our experiences in applying sound static code analysis to large-scale industrial software. While academia often focuses primarily on precision, analysis time, and memory consumption, industrial users require an additional emphasis on the presentation and visualization of results. Large-scale projects typically necessitate more abstract analyses, which inherently carry a higher potential for false alarms. Consequently, the explainability of findings becomes a critical factor for adoption.

    We discuss these requirements in detail, highlighting why explainability is paramount and how we adapted the reporting of runtime errors and signal flows to meet industrial demands.

    Our insights are derived from the domain of safety-critical embedded software, where stringent quality standards must be met. A core requirement of contemporary safety standards is the guaranteed absence of critical runtime errors. To address this, we utilize Astrée, a “second-generation” sound static analyzer for C/C++. While [1] demonstrates Astrée’s efficiency in handling large-scale automotive software for integration analysis, this talk delves deeper into the practical setup of these large analyses and the strategies used to present complex results to users.

    Furthermore, vehicle homologation often requires certification documentation that includes an analysis of all input/output signals influencing emissions-related components. [2] presents a sound non-interference analysis at the C/C++ level. This approach allows for the automated determination of signal dependencies and the verification of independence between specific inputs and outputs. In this talk, we summarize the underlying theoretical concepts, our industry-driven reworked taint propagation algorithm, and practical benchmarks from industrial projects. Special attention is given to how derived signal flows are visualized for the end-user.

    References:

    [1] Analyze this! Sound static analysis for integration verification of large-scale automotive software. D. Kästner, B. Schmidt, M. Schlund, L. Mauborgne et al. SAE Technical Paper 2019-01-1246, 2019.

    [2] Sound Signal Flow Analysis for C/C++. D. Kästner, L. Mauborgne, S. Hahn, S. Wilhelm, J. Herter, C. Cullmann, C. Ferdinand. Embedded World Congress 2025, Nuremberg.

  • 10:00 – Coffee break
  • 10:30 – Presentation of AnalyzeThat by the organizers
  • 10:40 – Result presentation by participating teams
  • 12:30 – Lunch
  • 14:00 – Result presentation by participating teams
  • 14:30 – Open discussion about identified challenges and future perspectives
  • 16:00 – Coffee break
  • 19:30 – Workshop Dinner
Back to top