Dagstuhl-Seminar 25421
Sound Static Program Analysis in Modern Software Engineering
( 12. Oct – 17. Oct, 2025 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/25421
Organisatoren
- Pietro Ferrara (University of Venice, IT)
- Liana Hadarean (Amazon Web Services - Seattle, US)
- Jorge Navas (Certora - Seattle, US)
- Caterina Urban (INRIA & ENS Paris, FR)
Kontakt
- Andreas Dolzmann (für wissenschaftliche Fragen)
- Susanne Bach-Bernhard (für administrative Fragen)
Gemeinsame Dokumente
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Impacts
- Try-Mopsa : Relational Static Analysis in Your Pocket : VMCAI 2026 accepted paper - Monat, Raphaël - Cornell University : arXiv.org, 2025. - 16 pp..
- Same Engine, Multiple Gears : Parallelizing Fixpoint Iteration at Different Granularities : extended version - Kocal, Ali Rasim; Schwarz, Michael -Singapore-; Saan, Simmo; Seidl, Helmut - Cornell University : arXiv.org, 2026. - 26 pp..
Programm
Motivation
Sound static program analysis (SSPA) applies formal methods to prove the absence of software defects, including runtime errors and security vulnerabilities. Although its foundational theories - most notably abstract interpretation - were developed nearly half a century ago, their practical adoption has been uneven. SSPA has become indispensable in safety-critical embedded systems, where software failures can have catastrophic consequences, yet it has historically seen limited uptake in desktop and Web applications. This divide has begun to narrow with the growing prominence of Web security threats, such as SQL injection attacks, and the rapid expansion of the Internet of Things (IoT). In today’s software ecosystem - dominated by microservices, serverless architectures, and dynamically typed scripting languages such as Python -- SSPA faces a renewed opportunity. Beyond bug prevention, it can offer structured, actionable feedback to a much broader community of developers, including practitioners without expertise in formal verification.
Despite these opportunities, SSPA faces significant challenges regarding the shift toward machine-learning-driven code generation and the complexity of multi-language architectures. Currently, many industrial players rely on shallow, syntactic analyses that leave systems vulnerable to serious flaws. To address this gap, this Dagstuhl Seminar "Sound Static Program Analysis in Modern Software Engineering" (25421) aimed at bridging the SSPA and software engineering scientific communities to adapt formal theories to modern trends. A primary focus was the integration of sound analysis into standard software development lifecycles and DevOps practices.
Summary of Seminar Activities
The Dagstuhl Seminar “Sound Static Program Analysis in Modern Software Engineering” (25421) was attended by 36 researchers, including both senior and junior participants from academia and industry, including graduate students, faculty members, and industry experts. At the beginning of the seminar, each participant briefly introduced themselves and outlined their research interests in a two-minute presentation.
The program interleaved 26 talks (Section 3 of the full report), two main breakout discussion sessions identifying and discussing open scientific problems (Section 4), and a “speed-dating” session in which participants were divided into Theory and Practice groups and engaged in a series of short, one-to-one discussions with members of the other group, rotating partners every 10 minutes.
Two invited talks provided perspectives from different points of view at the beginning of the seminar. In particular, Patrick Cousot discussed “Eternal Problems Never or Hardly Solved in Static Analysis by Abstract Interpretation” (Section 3.5 of the full report), while Davide Taibi tackled “Static Analysis in the Cloud-Native Era” (Section 3.24 of the full report). Most participants then illustrated their scientific progress in talks divided into sessions on security, data science programs, machine learning, concurrent software, program verification, heap analysis, and the precision of static analyzers. All together, the talks provided a deep, up-to-date, and some controversial views on the state of the art in SSPA and its application in software engineering practices. This was highly beneficial for sparking discussion of open scientific problems and potential industrial applications. Section 3 of the full report reports the abstracts of all the talks.
The breakout discussion sessions were organized into two main steps. During the first breakout session, the participants were randomly split into four distinct groups. Each group then had to identify the most compelling open problems in applying SSA to the software engineering lifecycle. A plenary discussion followed, during which participants identified the four open problems they considered most relevant. The outcome of this discussion is reported in Section 4.1 of the full report. In a subsequent discussion session, four groups (one for each open problem) were formed, and participants chose which group to join. Each group had a leader and reported the identified problems in a later plenary session. At the end of this discussion, the four most relevant open problems were the standardization of SSA components (Section 4.2 of the full report), the explainability of SSA results (Section 4.3), the interaction between LLMs and SSA (Section 4.4 of the full report), and how to push the adoption of SSA at the earlier phases of the software engineering process (Section 4.5of the full report).
Last but not least, various social activities took place every evening after dinner. These spanned from organized tournaments to informal board games. Section 5 of the full report reports all the results that were tracked during the seminar.
Conclusion
We consider the seminar a success. Altogether, it laid the basis for several tasks and follow-up:
- First of all, each of the four identified open problems represents a fundamental challenge for our community, and each group identified several actionable tasks that we expect the scientific community will target in future work;
- Most of the talks presented either preliminary results not yet published or assessed results with several future perspectives. The lively discussions that took place during the seminar will help the authors to improve the work and continue it in various directions, and other participants will take inspiration for their future work;
- Finally, the friendly atmosphere helped establish new connections through various social activities and informal networking. We expect this will open the door to new collaborations, hopefully leading to novel scientific publications and projects.
Creative Commons BY 4.0
Pietro Ferrara, Liana Hadarean, Jorge Navas, and Caterina Urban
Sound static program analysis (SSPA) can tackle real-world programs and effectively prove, for instance, that they do not expose some runtime errors and security vulnerabilities. Over the past half-century, many theories, all amenable to abstract interpretation, have been proposed and applied in practice: program analysis, program verification through SMT solvers, type systems, and model checking are just the most notable examples. SSPA has had a great impact on the analysis of safety-critical embedded software (where a single bug might cause catastrophic effects on the physical world) but has achieved so far limited interest in desktop applications (where bugs do not have relevant consequences). An exception is the revival of SSPA in Web applications, where a security vulnerability (such as a SQL injection) within them might have a relevant business impact. More recent developments, such as the Internet of Things, in the past decade, have bridged the realm of embedded software with Web applications.
Modern software architectures, such as microservices and serverless computing, incorporate multiple programming languages and technologies, requiring a substantial effort to formalize and implement sound semantics. However, such applications are limited in size and communicate through simple and clear interfaces (e.g., REST APIs). In addition, current trends underline a wider and wider adoption of scripting languages, such as Python, in different contexts. Applying SSPA in this context might provide deep and structured feedback to usually non-professional developers. Finally, the recent machine learning revolution has drastically changed how software is developed (from providing intelligent code completions and generating code snippets to fully developing software via model training). This poses novel challenges to SSPA regarding soundness, precision, and scalability. Unfortunately, all those opportunities have not seen a resurgence so far in applying SSPA to industrial software. The main players in the market apply shallow and syntactic analyses, exposing our society to serious flaws.
The main goal of this Dagstuhl Seminar is to bring together the sound static program analysis and the software engineering communities to stimulate the extension of existing theories to these new trends and to disseminate the practitioner community about what has been done so far in this field and what could be the further developments in the future. In particular, discussing how SSPA can be integrated into software engineering practices, such as DevOps and the overall software development lifecycle, seems essential for the successful application of SSPA to modern software development practices.
The objectives of the seminar are to:
- Bring together the scientific and industrial communities of static analysis and software engineering to discuss and investigate how sound tools (based on formal methods) can achieve a relevant impact on modern software engineering practices.
- Explore topics and calls for funding opportunities to develop projects applying sound static analysis in modern software engineering practices.
- Discuss challenges to formal methods arising from modern software architectures.
Pietro Ferrara, Liana Hadarean, Jorge Navas, and Caterina Urban
Please log in to DOOR to see more details.
- Vincenzo Arceri (University of Parma, IT) [dblp]
- Roberto Bagnara (University of Parma, IT) [dblp]
- Musard Balliu (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Valentin Barbazo (ENS, PSL University - Paris, FR)
- Anna Becchi (USI – Lugano, CH) [dblp]
- Dirk Beyer (LMU München, DE) [dblp]
- Patrick Cousot (New York University, US) [dblp]
- Eva Darulova (Uppsala University, SE) [dblp]
- Charles De Haro (ENS, PSL University - Paris, FR)
- David Delmas (Airbus - Toulouse, FR) [dblp]
- Giovanni Denaro (University of Milano-Bicocca, IT) [dblp]
- Werner Dietl (University of Waterloo, CA) [dblp]
- Elizabeth Dinella (Bryn Mawr College, US) [dblp]
- Greta Dolcetti (University of Venice, IT) [dblp]
- Pietro Ferrara (University of Venice, IT) [dblp]
- Isabel Garcia-Contreras (Black Duck - Calgary, CA) [dblp]
- Elisa Gonzalez Boix (VU - Brussels, BE) [dblp]
- Arie Gurfinkel (University of Waterloo, CA) [dblp]
- Liana Hadarean (Amazon Web Services - Seattle, US) [dblp]
- Kihong Heo (KAIST - Daejeon, KR) [dblp]
- Manuel Hermenegildo (IMDEA Software Institute - Madrid, ES) [dblp]
- Minseok Jeon (DGIST Institute of Science & Technology - Daegu, KR) [dblp]
- Tim King (Amazon Web Services - Santa Clara, US) [dblp]
- Valentina Lenarduzzi (University of Oulu, FI) [dblp]
- Debasmita Lohar (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Antoine Miné (Sorbonne University - Paris, FR) [dblp]
- Raphaël Monat (INRIA Lille, FR) [dblp]
- Naïm Moussaoui Remil (ENS, PSL University - Paris, FR)
- Jorge Navas (Certora - Seattle, US) [dblp]
- Guido Salvaneschi (Universität St. Gallen, CH) [dblp]
- Michael Schwarz (National University of Singapore, SG) [dblp]
- Helmut Seidl (TU München - Garching, DE) [dblp]
- Davide Taibi (University of Southern Denmark - Odense, DK) [dblp]
- Tian Tan (Nanjing University, CN) [dblp]
- Caterina Urban (INRIA & ENS Paris, FR) [dblp]
- Jingbo Wang (Purdue University - West Lafayette, US) [dblp]
Verwandte Seminare
- Dagstuhl-Seminar 23281: Theoretical Advances and Emerging Applications in Abstract Interpretation (2023-07-09 - 2023-07-14) (Details)
Klassifikation
- Logic in Computer Science
- Programming Languages
- Software Engineering
Schlagworte
- Static Program Analysis
- Abstract Interpretation
- Program Verification
