Dagstuhl-Seminar 23281
Theoretical Advances and Emerging Applications in Abstract Interpretation
( 09. Jul – 14. Jul, 2023 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/23281
Organisatoren
- Arie Gurfinkel (University of Waterloo, CA)
- Isabella Mastroeni (University of Verona, IT)
- Antoine Miné (Sorbonne University - Paris, FR)
- Peter Müller (ETH Zürich, CH)
Kontakt
- Marsha Kleinbauer (für wissenschaftliche Fragen)
- Christina Schwarz (für administrative Fragen)
Programm
Abstract Interpretation (AI) is a theory of the approximation of possible program behaviors. Since its introduction in the late 70s, it has evolved into a very general theory to describe and compare formal semantics of programs and systems. As a more practical aspect, it provides a formal framework to design effective static analyzers that are automatic, sound, and efficient. The last two decades have seen the emergence of practical tools now used routinely in the industry, starting with the embedded critical software industry and now being also applied to more mainstream software.
Despite its strength, designing new static analyses with AI remains a challenging task, involving both theoretical research and engineering efforts. The limited diffusion of AI knowledge in Universities, in Engineering Schools, and in the industry may hinder the development and more widespread use of AI-based tools. Moreover, the early focus on the verification of run-time errors in embedded software, while it provided a simpler and more controlled context than the general problem of verifying consumer software, and resulted in industrial successes, also could give the false impression that AI is only suitable for this task, while its theory is in fact much more general. Finally, the AI community has little interactions with that of other formal methods.
Based on these early observations, we set out to organize a Dagstuhl seminar on "Theoretical Advances and Emerging Applications in Abstract Interpretation" to discuss the state of the art in AI, identify its key challenges, and plan for its future. The seminar brought together 37 international experts in static analysis, from 10 countries, and from both academic and industrial background, covering a wide spectrum from pure Abstract Interpretation (AI) theory, to tool providers, to industrial users.
To provide a structure to the discussion, the seminar was organized as a series of topical days focusing on identified aspects (but not excluding other topics) of the state of the art and perceived challenges in AI: static safety verification, tools and applications, verification beyond safety analysis, and education. We proposed three invited talks and an invited tutorial of extended length (1h) and from key people in the community to bootstrap discussions on a variety of topics, ranging from theoretical AI to industrial tools, and providing historical perspectives. These were complemented with 23 shorter talks proposed spontaneously throughout the seminar. These talks, from 10min to 30min long, discussed a large variety of topics, including new research results, theoretical advances, experience reports, technical realizations, and reports on teaching activities. A significant number of presentations discussed connections of AI with other formal methods, including SMT solving, types, program logic.
During the seminar, we also organized several breakout sessions, where smaller working groups discussed a selection of topics: soundness requirements for static analysis tools, expressive domains, community infrastructure, education, connections with other formal methods, connections with machine learning, and tackling the verification of hyper-properties. As a conclusion of these working groups and the overall seminar, several tasks were started and a number of action items were proposed to advance further:
The group on soundness requirements proposed a first list of requirements that an analyzer should fulfill. It identified the need to discuss these findings with members of the soundiness manifesto, which raised awareness on the lack of proper requirements.
The group on community infrastructure proposed a series of practical actions to build the community on AI. It suggested the creation of a Special Interest Group in AI to coordinate the efforts.
The group on teaching started an on-going list (to be completed) of educational materials on AI. It presented the need to develop materials targeting undergraduate students and practitioners, to make efforts to better share available teaching resources, and to provide introductory courses on AI on MOOC platforms.
The group on the interaction between AI and other formal methods presented relevant connections with deductive verification, dynamic techniques, and model checking. In particular, it suggested the organization of a seminar on AI and deductive verification.
In general, this seminar expressed the interest to continue the discussion on the future of AI in further seminars focusing on specific challenges and opportunities as uncovered during the seminar, and adapting the list of participants in consequence.
Creative Commons BY 4.0
Antoine Miné, Arie Gurfinkel, Isabella Mastroeni, and Peter Müller
Abstract Interpretation (AI) has been introduced in the late 70s as a general theory to approximate the possible behaviors of computer programs. AI has since evolved into a very general theory to describe and compare formal semantics of programs and systems. AI introduces a formal notion of approximation, and rules to develop and design static program analyzers. Such analyzers run fully automatically (without user intervention), directly on the source code (not a model developed separately), and reason at an abstract level that forgets about irrelevant details to achieve an efficient analysis. AI provides mathematical tools to design abstractions that are sound by construction: Despite unavoidable loss of precision (incompleteness) caused by abstractions, analysis results are always trustworthy. AI promotes the design of reusable analysis building blocks, so-called abstract domains, and gives a principled, practical, and scalable framework for static analysis design.
Designing new static analyses is challenging and involves both theoretical research and software engineering: It requires the study of new abstract domains, tied to an application context (as there does not exist an all-purpose abstraction), and the design of efficient tools, finding the appropriate balance between cost and precision. Indeed, various developments in the last two decades have demonstrated that static analysis by AI works well also in practice. We have seen the emergence of commercially-available AI-based static analysis tools. Automation and efficiency make AI-based static analysis very attractive in such contexts. Moreover, soundness is also mandated by official documents (e.g., DO-333 in avionics). Nevertheless, early results on reachability analysis and a focus on embedded critical software (which have a simpler structure than typical consumer software) may propagate the false idea that AI is limited to detecting run-time errors in embedded code, while it is in fact far more general.
Now that AI has demonstrated its strengths in certain application domains, it is time to plan the future of AI, in particular, to widen its field of use beyond safety and static languages, and to bridge the gap between current theoretical results and practical applications by identifying key challenges, such as at targeting new languages, new classes of properties, and scalability to very large systems. Hence, the seminar aims at collecting new ideas and new perspectives on the potential of AI in order to pave the way for new applications of AI.
The objectives of this Dagstuhl Seminar are to:
- Bring together static analysis specialists from academia and industry to cover a wide spectrum from pure Abstract Interpretation (AI) theory to industrial tools.
- Discuss the current state of AI theory and applications, recent advances and roadblocks.
- Reconcile theoretical results and practical needs.
- Evaluate the most promising directions to drive forward fundamental research in AI and to push theoretic advances into practical tools.
- Take action to spread awareness of AI in universities, engineering schools, and in industry.
Arie Gurfinkel, Francesco Logozzo, Isabella Mastroeni, Antoine Miné, and Peter Müller
- Vincenzo Arceri (University of Parma, IT) [dblp]
- Musard Balliu (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Anna Becchi (Bruno Kessler Foundation - Trento, IT) [dblp]
- Dirk Beyer (LMU München, DE) [dblp]
- Bor-Yuh Evan Chang (University of Colorado - Boulder, US) [dblp]
- Patrick Cousot (New York University, US) [dblp]
- David Delmas (Airbus S.A.S. - Toulouse, FR) [dblp]
- Gidon Ernst (LMU München, DE) [dblp]
- Pietro Ferrara (University of Venice, IT) [dblp]
- Eden Frenkel (Tel Aviv University, IL)
- Isabel Garcia-Contreras (University of Waterloo, CA) [dblp]
- Roberto Giacobazzi (University of Verona, IT) [dblp]
- Roberta Gori (University of Pisa, IT) [dblp]
- Arie Gurfinkel (University of Waterloo, CA) [dblp]
- Reiner Hähnle (TU Darmstadt, DE) [dblp]
- Ben Hermann (TU Dortmund, DE) [dblp]
- Manuel Hermenegildo (IMDEA Software Institute - Pozuelo de Alarcón, ES & UPM - Madrid, ES) [dblp]
- Falk Howar (TU Dortmund, DE) [dblp]
- Temesghen Kahsai (Amazon Lab 126, US)
- Daniel Kästner (AbsInt - Saarbrücken, DE) [dblp]
- Matthieu Lemerre (CEA LIST - Gif-sur-Yvette, FR) [dblp]
- Isabella Mastroeni (University of Verona, IT) [dblp]
- Antoine Miné (Sorbonne University - Paris, FR) [dblp]
- Raphaël Monat (INRIA Lille, FR) [dblp]
- Peter Müller (ETH Zürich, CH) [dblp]
- Jorge Navas (Certora - Seattle, US) [dblp]
- Marie Pelleau (Université Côte d’Azur - Sophia Antipolis, FR) [dblp]
- Ruzica Piskac (Yale University - New Haven, US) [dblp]
- Francesco Ranzato (University of Padova, IT) [dblp]
- Gerhard Schellhorn (Universität Augsburg, DE) [dblp]
- Ilya Sergey (National University of Singapore, SG) [dblp]
- Sharon Shoham Buchbinder (Tel Aviv University, IL) [dblp]
- Mihaela Sighireanu (ENS Paris-Saclay - Gif-sur-Yvette, FR) [dblp]
- Yakir Vizel (Technion - Haifa, IL) [dblp]
- Thomas Wies (New York University, US) [dblp]
- Reinhard Wilhelm (Universität des Saarlandes - Saarbrücken, DE) [dblp]
- Enea Zaffanella (University of Parma, IT) [dblp]
Verwandte Seminare
- Dagstuhl-Seminar 25421: Sound Static Program Analysis in Modern Software Engineering (2025-10-12 - 2025-10-17) (Details)
Klassifikation
- Logic in Computer Science
- Programming Languages
- Software Engineering
Schlagworte
- Abstract Interpretation
- Abstract domains
- Static program Analysis
- Program verification
- Program semantics
