TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 25421

Sound Static Program Analysis in Modern Software Engineering

( 12. Oct – 17. Oct, 2025 )

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/25421

Organisatoren

Kontakt

Motivation

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.
Copyright Pietro Ferrara, Liana Hadarean, Jorge Navas, and Caterina Urban

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