Theoretical Advances and Emerging Applications in Abstract Interpretation

We consider the problem of making expressive static analyzers interactive. Formal static analysis is seeing increasingly widespread adoption as a tool for verification and bug-finding, but even with powerful cloud infrastructure it can take minutes or hours to get batch analysis results after a code change. While existing techniques offer some demand-driven or incremental aspects for certain classes of analysis, the fundamental challenge we tackle is doing both for arbitrary abstract interpreters. Our technique, demanded abstract interpretation, lifts program syntax and analysis state to a dynamically evolving graph structure, in which program edits, client-issued queries, and evaluation of abstract semantics are all treated uniformly.

The size and complexity of avionics software have grown exponentially from one aircraft generation to the next in the past 4 decades. Traditional software development processes leveraging informal verification techniques fail to scale within reasonable costs. In particular, verification is liable for a steadily growing share of the overall development costs. The 2015 current status was about 70.

To address this issue, Airbus have been transforming internal development processes since 2016. Internal domain-specific languages have been developed to enable the formalization of design artifacts, and automate part of verification activities. Automation is enabled by the interoperation of tools relying on sound formal techniques. For instance, Frama-C/WP and SMT-solvers are used to automate unit verification with deductive methods. Most so-called Unit Proofs are automatic, assuming high-level memory and numerical models, as well as some preconditions. Such assumptions are verified by other tools, such as the Astrée static analyzer, which leverages Abstract Interpretation to prove the absence of run-time errors and check assumed non-aliasing properties. We rely on the CompCert formally verified compiler to enable that most formal verification activities may be conducted on source code.

Beyond safety properties and currently established processes, we also develop internally static analyses by Abstract Interpretation to automate regression verification and portability verification. In particular, our portability analysis is able to prove without false alarms the portability of low-level C avionics software up to 1 million lines of C across platforms with opposite byte-orders (endianness).

We motivate the use of program transformation, traditionally used for the optimization of functional programs, as basic building blocks for lemma synthesis for recursive functions over algebraic data types. The key idea is to calculate at the function level instead of at the formula level, which allows one to work with intermediate syntactic functions. An important step therefore is to complement existing techniques (fixpoint fusion, deaccumulation) with capabilities to recognize when two functions are identical resp. share commonalities wrt. preconditions. The approach, work in progress, discovers typical distributive laws of list/tree functions like length, append, remove, which are similar in shape to those lemmas often required for data refinement proofs.

LiSA (LIbrary for Static Analysis – https://github.com/lisa-analyzer/lisa) is a Java library that implements the most common components of abstract interpretation-based static analyses. In this talk, we report our experience when adopting LiSA during courses at the master level focused on the theory of abstract interpretation. LiSA allowed students to implement, execute, and practice the theoretical concepts formalized throughout the course. However, it turned out that proper implementation of non-trivial abstract domains is beyond the capabilities of standard CS master students.

Often, verification of infinite-state and other complex systems, such as the Paxos consensus protocol, must work for unbounded domains. Quantified first-order logic allows us to reason over these unbounded domains, describe the desired behavior of these systems, and specify correctness properties. This is done by constructing formulas that describe the initial states of the system and its possible transitions, as well as formalizing the notion of illegal or unwanted states. A proof for the safety of a system then becomes an unreachability proof for the bad states, which can be provided via another formula, a safety invariant, which holds on the initial states, is invariant with respect to the transitions, and doesn’t hold on the bad states.

In this work we tackle invariant inference though the framework of abstract interpretation. We propose an algorithm that computes the strongest over-approximation of reachable states by iteratively sampling counter-examples to induction, but which is highly infeasible due to the magnitude of the abstract domain and SMT solver limitations. We proceed by presenting techniques based on syntactic subsumption that manage to avoid redundant formulas and explore an identically expressive search space exponentially more efficiently, and generalize to the abstract domain of first-order formulas.

Quantifier elimination (qelim) is used in many automated reasoning tasks including program synthesis, exist-forall solving, quantified SMT, Model Checking, and solving Constrained Horn Clauses (CHCs). Exact qelim is computationally expensive. Hence, it is often approximated. For example, Z3 uses “light” pre-processing to reduce the number of quantified variables. CHC-solver Spacer uses model-based projection (MBP) to under-approximate qelim relative to a given model, and over-approximations of qelim can be used as abstractions. In this talk, we present the QEL framework for fast approximations of qelim. QEL provides a uniform interface for both quantifier reduction and model-based projection. QEL builds on the egraph data structure – the core of the EUF decision procedure in SMT – by casting quantifier reduction as a problem of choosing ground (i.e., variable-free) representatives for equivalence classes. We have used QEL to implement MBP for the theories of Arrays and Algebraic Data Types (ADTs). We integrated QEL and our new MBP in Z3 and evaluated it within several tasks that rely on quantifier approximations, outperforming state-of-the-art.

Handling precise abstract values over large sets of program variables is costly. A solution is to split such “monolithic” values (over the whole set of program variables) into several subvalues over smaller subsets of variables. Applying abstract transformers separately to each subvalue is then more efficient than to the monolithic one, but typically incurs precision loss. To address this, one can transfer information between subvalues, a process known as reduction. Reduction is done iteratively by refining a subvalue using information from other subvalues until no values are further refined. Information transfer can be stopped at any time, guaranteeing soundness. Convergence is not ensured. In this talk, we study termination and precision properties of reduction from the perspective of logic. We define the notion of refutational equivalence between a monolithic and split value as a practical way to understand when a split domain is “precise enough”. Our main result is that if the theories used in the abstract domain admit and are closed uniform interpolation, reduction can be done in one step – by computing the uniform interpolant of the formula – guaranteeing refutational equivalence. For theories (or their combination) that do not admit uniform interpolation, or are not closed under uniform interpolation, we show that if a uniform interpolant is found, the reduction procedure can be immediately stopped, guaranteeing the best precision for the partitioned domain.

In this talk I will present some results concerning the bridge between the theory of computation and abstract interpretation. The two theories differ profoundly in the way programs are interpreted: In the standard theory of computation program equivalence is extensional, we have compositionally and referential transparency. Abstract interpretation instead is deeply intensional, non compositional (in the sense that by composition we may lose precision). However, it is possible to view the theory of abstract interpretation from the perspective of the theory of computation. In this case a different notion of program equivalence is considered – the one defined by the equivalence of the abstract interpretations, and push the theory of abstract interpretation to its limits by studying the properties of abstraction that make an abstract interpretation closer to the standard notion of interpretation as originally defined by A. Turing. Interestingly, a analogous of Rice Theorem can be stated for abstract interpretation and a number of results can be obtained for classes of programs for which an abstract interpreter is precise (complete).

To address bug finding rather than correctness, Incorrectness Logic has been recently proposed by O’Hearn: it is based on under-approximations, thus it only reports true alarms. In principle, Abstract Interpretation techniques can handle under-approximations as well as over-approximations, but, in practice, few attempts were developed for the former, notwithstanding the wide literature on the latter. We aim to answer the following open question raised by O’Hearn: which role can Abstract Interpretation play in the development of under-approximate tools for bug catching? Our findings clarify, for the first time, why over- and under-approximation analysers exhibited such a different development and outline the limits of under-approximation Abstract Interpretation based analyses. Our key argument is the practical difficulty to design an effective under-approximation abstract domain able to deal with common program statements. For this reasons we investigate logics for underapproximations. We introduce Sufficient Incorrectness Logic (SIL), a new under-approximating, triple-based program logic to reason about program errors. SIL is designed to set apart the initial states leading to errors. We formally compare SIL to existing triple-based program logics.

We demonstrated how the integration of the Ciao abstract interpretation framework within different IDEs takes advantage of our efficient and incremental fixpoint to achieve effective verification on-the-fly, as the program is developed. We also demonstrated an embedding of this framework within the browser, and how it can be used to build interactive tutorials for teaching abstract interpretation.

Automated reasoning techniques offer an exceptional avenue to attain the utmost assurance in safeguarding data privacy. In this presentation, we will explore our adaptations of these techniques in addressing vital inquiries concerning code and cloud infrastructure, aimed at identifying potentially harmful misconfigurations. We will delve into the deployment of highly scalable static analysis for sensitive data tracking, the utilization of a provably correct differential privacy library to guarantee the safety of shared aggregated data, and the implementation of diverse pseudo-anonymization methods to safeguard sensitive information.

The presentation gives a brief overview of the verification goals addressed by the Astrée analyzer, and then focuses on the development history from the ready-for-market academic version from 2009 till today’s state. Enhancements are grouped into different categories, usability, compliance to formal requirements, new capabilities, domain-specific extensions, precision improvement and optimizations for scalability. The current state is briefly summarized by experimental results on automotive integration analysis projects, taken from our 2023 SAE conference paper. We then briefly summarize “selling points” of verification tools to industry users with an emphasis on the role of safety norms: they define the minimum state of the art for system development and play a fundamental role in the adoption of tools in industrial development processes. We give examples how abstract interpretation is addressed in DO-178C and ISO 26262, observe that it is entirely missing in others, and conclude that it is under-representated in today’s safety norms. The presentation ends with listing some verification challenges we see upcoming due to current market trends.

Conversion to Static Single Assignment (SSA) form is usually viewed as a syntactic transformation algorithm that gives unique names to program variables, and reconciles these names using “phi” functions based on a notion of domination. We instead propose a semantic approach, where SSA translation is performed using a simple dataflow analysis. Based on a new technique to use cyclic terms in abstract domains, we propose a Symbolic Expression abstract domain that performs a Global Value Numbering analysis, upon which we build our SSA translation. This implies a shift in perspective, as global value numbering becomes a prerequisite of SSA translation, instead of depending on SSA.

One application to performing SSA Translation by Abstract Interpretation is that SSA optimizations passes can be implemented as a combination of abstract domains, allowing to perform several optimizations simultaneously to solve the usual phase ordering problem and avoiding tedious maintenance of SSA invariants.

Our main motivation for this research is an analyser for machine code which uses SSA as its main intermediate representation. Machine code is too low-level to allow SSA translation without a prior semantic analysis, while SSA is an intermediate representation that makes static analysis easier than direct analysis of machine code. Viewing SSA translation as a semantic analysis solves this chicken-and-egg problem, allowing to simultaneously decompile machine code to SSA and use the SSA representation to perform the other semantic analyses (value analysis, memory analysis, and control-flow analysis). We illustrate the use of such an analysis on an embedded OS kernel where we prove security properties directly from its executable.

Mopsa is a conservative static analysis platform, independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision. In this talk, we will show how Mopsa analyses Python programs calling C libraries. It analyses directly and fully automatically both the Python and the C source codes. It reports runtime errors that may happen in Python, in C, and at the interface. We implemented our analysis in a modular fashion: it reuses off-the-shelf C and Python analyses written in the same analyzer. Our analyzer can tackle tests of real-world libraries a few thousand lines of C and Python long.

This talk is based on our SAS’21 paper.

Crab is an open-source library that helps to develop static analyses based on the theory of Abstract Interpretation. It provides a variety of software components such as inter-procedural forward and backward analyses, fixpoint solvers and a rich set of abstract domains, including interfaces with numerical abstract domain libraries such as Apron, Elina or PPLite.

This tutorial focuses on demonstrating how to use Crab from the perspective of two different kinds of users: (1) the ones who want to quick prototype new abstractions by combining existing abstract domains, and (2) those who want to develop new static analyses using Crab as a black-box. We show several interactive demos on how to derive new abstractions based on the combination of an array domain with relational numerical domains to prove memory safety of eBPF programs and how to implement a new LLVM-based static analyzer to infer upper-bounds for dynamic memory allocation in less than 100 lines of C++ code.

We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural relational semantics covering both finite and infinite executions. This understanding of logics as abstractions of a semantics facilitates their comparisons through their respective abstractions of the semantics (rather that the much more difficult comparison through their formal deductive systems). More importantly, the formalization provides a calculational method for constructively designing the sound and complete formal deductive system by abstraction of the semantics. As an example, we extend Hoare logic to cover all possible behaviors of nondeterministic programs and design a new precondition (in)correctness logics. This logic can be used to prove that false alarms in static analysis are due to the over approximation of nonterminating behaviors by terminating over approximation in the analysis which cannot be done by incorrectness or outcome logic is unreachable in the concrete (although it is reachable in the abstract).

The field of formal methods relies on a large body of background knowledge that can dissuade researchers from engaging with younger students, such as undergraduates or high school students. However, we have found that formal methods can be an excellent entry point to computer science research – especially in the framing of Computing Identity-based Mentorship. In this talk, we report on our experience in using a cascading mentorship model to involve early stage researchers in formal methods, covering the process with these students from recruitment to publication. We present case studies and how we were able to integrate formal methods research with the students’ own interests. We outline some key strategies that have led to success and reflect on strategies that have been, in our experience, inefficient.

We introduce a program logic, called Local Completeness Logic for an abstract domain $A$ (LCL_A), for proving both the correctness and incorrectness of program specifications. This proof system, which is parametrized by the abstraction $A$, combines over- and under-approximating reasoning: in a provable triple ${⊢}_A[p]c[q]$ for the program $c$, $q$ is an under-approximation of the strongest post-condition of $c$ on input pre-condition $p$, such that their abstractions in $A$ coincide. If $A$ is the straightforward abstraction making all program properties equivalent, then the logic LCL_A coincides with O’Hearn’s incorrectness logic. We discuss the pitfalls of this logic LCL_A and why it is hard to make proofs within it. We, therefore, advocate designing a weakening of LCL_A which should be able to prove properties of program analyses rather than program behaviors, in particular for proving that a program analysis is the best possible one in the underlying domain $A$.

The talk presented the new VeriCode project (funded by German Research Foundation DFG) we just started. The projects aims at the generation of efficient code from abstract specification. Such specifications are typical when using higher-order logic and abstract programs to specify functions. They typically use abstract datatypes which are easily translated to functional code. However the resulting code is typically not very efficient and requires garbage collection. The project was motivated by an earlier DFG project called Flashix that produced a verified file system for flash memory. A simple code generator is already implemented that produces C- and Scala-Code, based on the principle that in contrast to a functional implementation data structure should not share. The approach enables destructive updates and allows to avoid garbage collection. The approach still causes too much copying and the talk showed some first optimizations. Compared to a native implementation of a flash filesystem (UBIFS) in C that we used as a blueprint, our code is still some factors slower and the project aims to close the gap. The talk also showed the overall approach of the project, which is not just to implement an efficient code generator, but to verify that it is correct again using specifications of the relevant functionality and semantics. Ultimately this should allow to bootstrap the code generator by again generating code from the specification of its functionality.

Implementing bug-free concurrent programs is a challenging task in modern software development. State-of-the-art static analyses find hundreds of concurrency bugs in production code, scaling to large codebases. Yet, fixing these bugs in constantly changing codebases represents a daunting effort for programmers, particularly because a fix in the concurrent code can introduce other bugs in a subtle way.

In this talk, I will show how to harness compositional static analysis for concurrency bug detection, to enable a new Automated Program Repair (APR) technique for data races in large concurrent Java codebases. The key innovation of our work is an algorithm that translates procedure summaries inferred by the analysis tool for the purpose of bug reporting into small local patches that fix concurrency bugs (without introducing new ones). This synergy makes it possible to extend the virtues of compositional static concurrency analysis to APR, making our approach effective (it can detect and fix many more bugs than existing tools for data race repair), scalable (it takes seconds to analyse and suggest fixes for sizeable codebases), and usable (generally, it does not require annotations from the users and can perform continuous automated repair). Our study conducted on popular open-source projects has confirmed that our tool automatically produces concurrency fixes similar to those proposed by the developers in the past.

Inferring inductive invariants is one of the main challenges of formal verification. One of the latest breakthroughs in invariant inference is property-directed reachability (IC3/PDR). In this talk, we utilize the rich theory of abstract interpretation to shed light on the overapproximation of the reachable states performed by PDR’s frames. Namely, we define an eager version of PDR, called Lambda-PDR, in which all generalizations of counterexamples are used to strengthen a frame, and show that its frames can be formulated as an abstract interpretation algorithm in a logical domain based on Bshouty’s monotone theory. Since the frames of Lambda-PDR are tighter than the frames of PDR, the same overapproximation, and more, is present in PDR’s frames. We demonstrate that this overapproximation can result in an exponential gap compared to exact forward reachability.

Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers and it formalizes a cooperation between static analyzers doing pointer analysis and a deductive verification tool based on first order logic. We propose a framework based on memory models that captures the partitioning of memory inferred by pointer analyses, and complies with the memory models used to generate verification conditions. The framework guided us to propose a pointer analysis that accommodates to various low-level operations on pointers while providing precise information about memory partitioning to the deductive verification. We implemented this cooperation inside the Frama-C platform and we show its effectiveness in reducing the task of deductive verification on a complex case study.

Condition synthesis takes a program in which some of the conditions in conditional branches are missing, and a specification, and automatically infers conditions to fill-in the holes such that the program meets the specification.

In this talk, we present CoSyn [1], an algorithm for determining the realizability of a condition synthesis problem, with an emphasis on proving unrealizability efficiently. CoSyn is baed on a reduction of the condition synthesis problem to satisfiability of Constrained Horn Clauses (CHCs). In order to allow this reduction to CHCs, we use the novel concept of a doomed initial state, which is an initial state that can reach an error state along every run of the program. For a doomed initial state $\sigma$, there is no way to make the program safe by forcing $\sigma$ (via conditions) to follow one computation or another. CoSyn encodes the existence of a doomed initial state as CHCs.

CoSyn is implemented in SeaHorn using Spacer as the CHC solver and evaluated it on multiple examples. The evaluation shows that CoSyn outperforms the state-of-the-art syntax-guided tool Cvc5 in proving both realizability and unrealizability. Evaluation also shows that joining forces of CoSyn and Cvc5 outperforms Cvc5 alone, allowing to solve more instances, faster.

Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constrained Horn clauses extracted from typing derivations. An example is Liquid type inference, which solves the extracted constraints using predicate abstraction. However, the reduction to constraint solving in itself already signifies an abstraction of the program semantics that affects the precision of the overall static analysis. To better understand this issue, we study the type inference problem in its entirety through the lens of abstract interpretation. We propose a new refinement type system that is parametric with the choice of the abstract domain of type refinements as well as the degree to which it tracks context-sensitive control flow information. We then derive an accompanying parametric inference algorithm as an abstract interpretation of a novel data flow semantics of functional programs. We further show that the type system is sound and complete with respect to the constructed abstract semantics. Our theoretical development reveals the key abstraction steps inherent in refinement type inference algorithms. The trade-off between precision and efficiency of these abstraction steps is controlled by the parameters of the type system. Existing refinement type systems and their respective inference algorithms, such as Liquid types, are captured by concrete parameter instantiations.

Hard real-time systems need a proof that they keep their deadlines. This proof is produced by a code-level WCET analysis and a schedulability analysis for a set of tasks to be executed on the same platform. A code-level WCET analysis computes a safe upper bound for all execution times of a task. The only sound WCET analysis used widely in industry, developed by my group in Saarbrücken, uses several abstract interpretations to safely and efficiently derive such upper bounds for tasks to be executed on single-core platforms. Central for the practicality of our approach are adequate abstractions of the architecture of the execution platform. Thus, the architecture is an integral part of the semantics from which abstract interpretations of real-time programs are derived. This entails a number of peculiarities compared to more conventional abstract interpretations. They are more concerned with the occupancy of platform resources than with the values contained in those resources. The occupancy of resources, e.g. the cache contents or the usage of bus bandwidth influence the timing behavior. Iteration over loops, as part of the fixed-point iteration, needs to consider machine parameters to achieve accuracy. The first iteration of a loop typically loads the cache, and later iterations profit from this cache loading. Therefore, first and non-first iterations may have vastly different execution times. In order to obtain accurate execution times for loops, the iteration of the analysis first needs to stabilize the execution time of the loop body. In my talk I gave some such examples of peculiarities [2]. The main part was concerned with the development history of our WCET-analysis technology [1].

We discussed abstract domains for data structures and domains that can capture complex properties. We observed that a large variety of techniques have been described in the literature, e.g., for the data structures sequences/strings, sets, multisets, arrays, pointer-structures, and trees/general ADTs, and which e.g., can express properties like sortedness or initialization. However, while for numerical domains, we have nice open-source libraries that can easily be embedded into larger use-cases, it was noted that this is hardly the case for such expressive domains despite the fact that there are many implementations. We then discussed the challenges in the design of both the domains itself as well as a uniform interface that could capture their features and commonalities: The first challenge is to define a common interface in the first place. Since domains are usually designed to tackle specific properties, the operations they offer are tuned to their respective use cases and therefore not uniform. As an example, it seemed unclear whether it is possible to represent the features offered by domains as part of a CHC solver. As possible future work, a first step towards usable off-the-shelf libraries was to investigate the design of a suitable API. A second challenge is the combined use of abstract domains, for example when nesting domains for element types inside container types. There is no canonical choice to do so many, and which is appropriate strongly depends on the application. This kind of integration often relies on the tight integration of the data structures representing the abstract domains at the implementation level. This kind of compositionality, however, is hard to achieve general because domains – even for the same purpose – may rely on rather different techniques. A related problem is how to provide on-line transfer from and to symbolic representations. We idientified as a question for the efficient combination of domains, whether some of the higher-level domains benefit from some specialized operators of the underlying abstract domains. The third challenge is that it is hard to design abstract domains that are robust. A lot of knowledge goes into selecting the right abstraction for a given (sub-)problem and choosing the an inappropriate one incurs high computational cost. Unfortunately, this is hard to determine automatically, and moreover may rely on user-provided partial specifications as guidance.

During this working group, the discussion was divided into two main themes: teaching to graduate students, and to undergraduates or, generally speaking, practitioners. In the first case, a lot of good material is available. A non-comprehensive list (that should be further integrated) to the best of the participants’ knowledge is the following one: books [1, 2]; slides [3, 4, 5, 6, 7, 8]; tools [9, 10].

For undergrads and/or practitioners there is less material available. After an open discussion with all the seminar participants, we were able to assemble the following list: [11, 12, 13].

Generally speaking, the first idea would be to augment undergraduate courses on the implementation of interpreters with the idea of abstraction (e.g., [7]). Another proposal was to design a generic interface to interact (ranging from the application to the extension) with static analyzers through a unique library, avoiding having analyzers that require being bound to specific programming languages. This is a rather standard approach adopted by our communities that over the years achieved better visibility and popularity (e.g., the machine learning community with libraries such as Scikit-learn and Pytorch, or the theorem-proving community with libraries such as SMT-lib).

Overall, the participants agreed that the community is missing a place where educational material about static analysis can be shared, as well as introduction courses in popular MOOC platforms.

The main outcome of this working group was a proposal to build up a community infrastructure to facilitate the promotion of events in our community, stimulate interactions, and provide better visibility of the main outcomes in our field. In particular, currently, we have various groups on social networks (such as Facebook and Linkedin) that are mostly silent. However, every year we have a series of regular events that help the networking activities of our community, such as conferences like SAS and VMCAI, workshops like SOAP, and events organized by various institutions such as the “Dependable and Secure Software Systems” workshop at ETH or the Challenges of Software Verification Symposium at Ca’ Foscari University of Venice (just to name a few the participants were aware of, but such a list should be quite expanded).

The final proposal of the working group was to: (i) build up a website that contains information about events and materials about static analysis (taking inspiration from https://microservices.community), (ii) open a mailing list about announcements regarding scientific activities and opportunities in static analysis, and (iii) establish an Interest Group in Static Analysis (IGSA) with an advisory board that supervise the overall process. Potentially this might become an ACM Special Interest Group, an IFIP Working Group, or something else, based on the success of the initiative.

This working group discussed potential new connections between Abstract Interpretation and other Formal Methods. Based on the interests and expertise of the participants, the other formal methods that the group focused on were: Deductive Verification, Dynamic Techniques, Deduction, Model Checking, and Practical and Industrial applications.

For deductive verification, there is a desire for Abstract Interpretation to infer complex specifications, especially in the context of memory analysis. Currently, most developed Abstract Interpretation techniques are geared towards numeric domains that are not sufficiently structurally complex (i.e., no quantifiers, no memory separation, etc.). Deductive verification also requires very reliable tools that reliably provide an answer since such tools involve a direct and active interaction with a user.

For dynamic techniques, there is a desire for better abstract domains for strings. Perhaps based on the deep connection between automata and regular languages. There is also a potential in using dynamic analysis to infer context for Abstract Interpretation-based static analysis. This, for example, is already used in debloading projects such OCCAM at SRI. The group felt that this combination might also create new challenges to maintaining soundness of the analysis and/or articulating the soundness conditions clearly.

For deduction, it was discussed that the main challenge is to identify an insight for why a proof works or fails. In this context, a complex but hard-to-understand specification, such as an automatically generated inductive invariant, is not very helpful. Perhaps the results of Abstract Interpretation can be presented in a more readable form by using some pre-defined set of predicates.

For model checking, there is an interest in building Abstract Interpretation models that explain core model checking algorithms such as IC3 and PDR. There is recent work on this subject, but the group agrees that better understanding is required to capture the many nuances of these algorithms. There is also a potential application in using Abstract Interpretation to infer temporal specifications.

Group members from industry, were interested in Abstract Interpretation for probabilistic programs, with application to differential privacy. There is also interest in Abstract Interpretation in aid of property-based testing.

Overall, the working group concluded that there is a lot of interest in both applications of Abstract Interpretation in different domains, and in research on challenges that are posed by these domains. The group members from Deductive Verification have been most vocal, and, perhaps the combination of Abstract Interpretation and Deductive Verification is most suited for a follow up seminar.

We had a discussion on challenges that developers of research tools must address to enable industrial collaborations and on possible working directions for the research community to foster the development of robust and scalable research tools. Among the attendees were researchers, academic tools developers, as well as developers of commercial tools and industrial researchers from companies that use formal methods tools in their product development, presenting both, academic perspectives, and insights from industry.

The initial focus of the discussion was on the potential and challenges of using research tools effectively in real-world scenarios and started with the observation that it is often difficult to use research tools in industrial collaborations.

Lessons learned by academic developers included the following points:

Usefulness: It is important to have findings and to make these findings accessible to project partners, who typically are not experts in a particular formal method or a particular research tool.

Robustness: It is important that tools can be used in industrial settings. This often requires operation in an automated analysis pipeline, e.g., a build system. In such a setting, an analysis will not be run manually executed one target but is executed as part of a build process.

Participants from companies complemented these observations with the following points:

Helpful features: To support robustness, certain features help applicability that are (usually) not important in an academic context: since industrial codebases in many cases cannot be extended with annotations for a tool, it is important to support declarative configurations and external annotations. Usefulness can be increased by support for problem extraction (i.e., interpretation / mapping of results to code) and by providing information on relationships between alarms (i.e., root causes).

Project formats: Analyzing an industrial codebase is not an easy task, especially when done by someone who is not a contributor to that codebase. Typically, success hinges on support from developers, access to architecture documentation, and on communication between maintainers and researchers. Project formats should accommodate these success factors.

Licenses: Copyleft licenses are a big obstacle in industry if code is under such a license and the industrial partner must look at the code (e.g., to understand how a tool work).

Eventual Payoff: It is important for industrial partners to understand if and what the eventual payoff can be when using a technique or tool. As a concrete successful example, the technique of unit proving was mentioned. In the experience of one participant, maintainability and conformance to low level specs seems to be much easier with unit proving than with testing once it is established in the development process.

After the initial collection of lessons learned, discussion evolved around dealing with theoretical limitations of techniques and (potential) usability requirements.

Dealing with Limitations: Commercial tool developers (AbsInt and Astree tools) reported that in their experience mostly scalability and precision are bottlenecks and that proofs tend to work on slices, but do not work on whole programs. It was discussed if and to what extend a target can be modified in order to scale or work around limitations (e.g., loop unrolling, transformations at the IR level). Consensus was that, while it is usually not possible to change a customer’s code, transformations typically happen during analysis (with some limitations in safety-critical domains). It was deemed important that the result/verdict of an analysis can be explained to the user and in terms of the original code.

Usability: There was no consensus on or shared understanding of usability requirements. Most participants agreed that a user interface is not a strong requirement for a research tool, but that usability is still important in the sense that users need to be able to understand the findings of a tool (e.g., based on CFGs).

The discussion concluded with plans for actions the research community could take to recognize and facilitate the development of robust research tools. Case studies were identified as a relevant format: It shows potential users how a tool can be used on a realistic example and forces developers to invest in robustness and applicability. Examples of existing case studies and publicly available systems included the effort to verify the Linux kernel, medical systems (e.g., infusion pumps, a pacemaker), and a wheel-break system. Participants agreed that it will be important to promote case study papers in academic conferences. Published case studies should include a public repository with the problem, corresponding artifacts (e.g., documentation), and an experience report.

Hyperproperties are intended as sets of sets of traces, for a more general point of view, we can see them as sets of properties. A standard example of hyperproperty is non-interference, a 2-safety property that requires to compare pairs of executions. The question for stimulating the discussion was about the right implication formalization for hyperproperties. In the literature we mainly find two different approaches: (1) The first one allows to add new elements in the hyper set, but all the elements in the stronger property must be in the weaker one, more formally, let $A,B,C,D,E$ sets, then $\{A,B,C\}$ implies $\{A,B,C,D,E\}$; (2) the second one consists in allowing to approximate the inner elements without adding any new element, formally let $A,B,C,A^{\prime },B^{\prime },C^{\prime }$ be sets such that $A\subseteq A^{\prime }$, $B\subseteq B^{\prime }$ and $C\subseteq C^{\prime }$, then $\{A,B,C\}$ implies $\{A^{\prime },B^{\prime },C^{\prime }\}$ but $\{A,B,C\}$ does not imply $\{A^{\prime },B^{\prime },C^{\prime },D^{\prime }\}$ where $D^{\prime }$ does not contain any of $A,B,C$. Hence, which of these orders properly capture the approximation order between hyperproperties.

There are several approaches to noninterference that can help in understanding the issue, in particular those based on hyper analysis of programs. But also there are other relevant formal approaches to hyper properties verification, such as the hyper Hoare logic, useful for understanding the issue.

By reasoning on both these formal approaches, the discussion ended up understanding that probably there is no a right or better order, in particular (2) is necessary for computing fixpoints programs/properties in an hyper levels both in the analysis and in the logic, while (1) is used for deciding whether a property imply another one, again both in the analysis and in the logic (consequence rule). Hence, the conclusion was that (1) is the approximation order while (2) is the computational order, which maybe must co-exists when dealing with hyper property verification. We believe that this final observation, even if it may appear quite “simple”, may represent anyway an important first step for really understanding the connection between standard approaches to static analysis and the emerging hyper property verification issue. All participants agree that surely further understanding of the problem is necessary.

A small working group entitled “AI for AI” discussed existing and possible future interactions between Abstract Interpretation (AI) and Machine Learning (ML). Both directions, AI to help ML and ML to help AI, were considered.

We started with the observation that, with the progress and increasing use of ML systems, ensuring their correctness also became an increasing concern. Since 2015, the field of formal verification techniques applied to ML systems has been growing steadily. A large amount of work targets the verification of trained neural networks, but other models are considered as well (e.g., support vector machines, ensemble trees). Moreover, many kinds of formal methods have been adapted to work on ML systems, including: SMT solving, constraint solving, optimisation, model-checking, Abstract Interpretation. Notable works on Abstract Interpretation for ML models include the developments of dedicated numeric abstract domains able to prove local robustness properties and fairness properties. A more detailed review of recent work can be found in Urban et al. 2021 [1]. However, given the pace of the research in this area, such reviews become outdated very quickly.

We then discussed what we perceived as some of the current limitations of AI methods for ML and possible area of improvements.

• $\mathrm{■}$

  The verification of robustness has been successful for models of moderate size, and for local robustness against perturbation and adversarial attacks. Future challenge concern more global robustness properties. Numeric abstractions and partitioning techniques from AI could be key to achieve scalability.

• $\mathrm{■}$

  ML research has recently focused on interpretability and explainability of ML models. This constitutes an interesting opportunity to apply formal verification and obtain sound and automatic guarantees on these properties. We postulate that AI-specific techniques, such as relational abstractions, might help in evaluating out inputs influence the outcome of a ML model.

• $\mathrm{■}$

  In general, however, a key difficulty for formal verification (including Abstract Interpretation) is the lack of formal specification of the properties to prove. This is an area that must be improved in order to unlock further progress.

• $\mathrm{■}$

  Most works in ML ignore the effect of floating-point rounding errors. AI techniques exist to soundly verify floating-point programs and to evaluate the effect of rounding errors formally. Applying such techniques to ML models could prove useful.

The working group also considered how ML could help AI. An important aspect is to keep the formal guarantees of the combined AI and ML method by maintaining soundness, even in the absence of soundness guarantees for the ML part.

• $\mathrm{■}$

  One possible use of ML in AI is the automatic parameterization of static analyzers to optimize the efficiency and precision of the analysis within the parameter space (e.g., choice of abstract domains, level of relationality and sensitivity, etc.).

• $\mathrm{■}$

  A specific aspect of AI is the use of widening operators to automatically infer complex invariants. The heuristic nature of widenings makes them an interesting target for ML techniques: the heuristics “guessing” candidate invariants do not need strong soundness guarantees, given that candidate invariants can be checked with a classic, sound stability tests. This idea could be extended to the inference of contract pre/post-conditions to unlock efficient modular analyses.

As concluding remark, we observed that early research in formal verification of ML was mainly conducted by formal method researchers, adapting on ML models the techniques they were familiar with for the verification of software. Given the substantial differences between ML models and programs, and the need to extract and formalize the properties we are interested to verify on ML models, we believe that progress in this field requires a tighter collaboration of experts in ML and experts in AI.