TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 20251

Theoretical Advances and Emerging Applications in Abstract Interpretation Postponed

( Jun 14 – Jun 19, 2020 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/20251

Replacement
Dagstuhl Seminar 21211: Theoretical Advances and Emerging Applications in Abstract Interpretation (2021-05-24 - 2021-05-28) (Details)

Organizers

Contact

Motivation

Abstract Interpretation has been introduced in the late 70s as a general theory to approximate the possible behaviors of computer programs. Abstract Interpretation has since evolved into a very general theory to describe and compare formal semantics of programs and systems.

Abstract Interpretation 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. Abstract Interpretation 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. Abstract Interpretation 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 Abstract Interpretation works well also in practice. We have seen the emergence of commercially-available Abstract Interpretation based static analysis tools. Automation and efficiency make Abstract Interpretation 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 Abstract Interpretation is limited to detecting run-time errors in embedded code, while it is in fact far much more general.

Now that Abstract Interpretation has demonstrated its strengths in certain application domains, it is time to plan the future of Abstract Interpretation, 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, this Dagstuhl Seminar aims at collecting new ideas and new perspectives on the potential of Abstract Interpretation in order to pave the way for new applications of Abstract Interpretation.

The objectives of the seminar are to:

  • Bring together static analysis specialists from academia and industry to cover a wide spectrum from pure Abstract Interpretation theory to industrial tools.
  • Discuss the current state of Abstract Interpretation theory and applications, recent advances, and roadblocks.
  • Reconcile theoretical results and practical needs.
  • Evaluate the most promising directions to drive forward fundamental research in Abstract Interpretation and to push theoretic advances into practical tools.
  • Take action to spread awareness of Abstract Interpretation in universities, engineering schools, and in industry.
Copyright Arie Gurfinkel, Francesco Logozzo, Isabella Mastroeni, Antoine Miné, and Peter Müller

Participants
  • Arie Gurfinkel (University of Waterloo, CA) [dblp]
  • Francesco Logozzo (Facebook - Seattle, US) [dblp]
  • Isabella Mastroeni (University of Verona, IT) [dblp]
  • Antoine Miné (Sorbonne University - Paris, FR) [dblp]
  • Peter Müller (ETH Zürich, CH) [dblp]

Classification
  • semantics / formal methods
  • verification / logic

Keywords
  • Abstract Interpretation
  • Abstract domains
  • Static program Analysis
  • Program verification
  • Program semantics