Sound Static Program Analysis in Modern Software Engineering

While concurrency can achieve significant performance improvements, it also introduces an additional layer of complexity in program design. Synchronization mechanisms are required to prevent data races on shared resources, which could otherwise lead to inconsistent results or data corruption. For instance, pointer updates by one thread may render some memory regions unreachable to others, thereby invalidating their assumptions about shared data. In this talk I present ongoing work toward a shape analysis for concurrent programs based on non-blocking synchronization mechanisms. Our goal is to prove the preservation of structural properties of dynamically allocated data structures shared across multiple threads. Our approach builds on previous work describing how to embed Rely-Guarantee reasoning in the Abstract Interpretation framework [1]. I describe our current progress on the design of an effective thread-modular shape analysis leveraging existing separation-logic-based memory abstract domains to precisely capture and account for thread interactions.

Quantifier elimination (QE) is a key task in formal verification algorithms. An important feature of QE is the ability to return partial results when interrupted early: a notable example is Model-Based Projection (MBP), a technique used to return an under-approximation of QE. Another desirable feature of QE is that the output is returned in a concise representation. In the theory of Linear Rational Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity, that is, they return a disjunction even for a conjunctive input, or they return a large non-minimal representation. This can disadvantage the QE client. To address these issues, we introduce the new concept of Bidirectional Model-Based Projection (BMBP). Given a model, BMBP returns both an over- and an under-approximation of QE. We define a new QE algorithm for LRA (BMBP-QE) that (i) is an anytime algorithm capable of providing two complementary partial results – a conjunctive over-approximation and a disjunctive under-approximation – when interrupted early, (ii) returns a minimal conjunction when the input is conjunctive, and (iii) applies to arbitrary LRA formulae. Given the twofold nature of the partial results, BMBP has the potential to enable new strategies in verification algorithms currently relying on MBP. BMBP also benefits QE clients by returning a minimal representation for conjunctive inputs. We show that our algorithm does not introduce significant overhead compared to QE methods using MBP. In fact, BMBP-QE outperforms SMT-based QE algorithms, offering improvements in both runtime and result size.

There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries (block contracts) are computed – based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (computed from postconditions received from block predecessors, i.e., which program states reach this block) and violation conditions to check at the block exit (computed from violation conditions received from block successors, i.e., which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a postcondition or violation condition) is available from other blocks, the verification can decide to restart with this new information. We formulate our approach as configurable program analysis and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well, and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.

I tried to remember the history of the discovery of the principles of abstract interpretation and collect problems that remain challenging, some over 50 years, like definition of the semantics of programming languages, efficiency, soundness, scalability, study of the discovery of inductive arguments in inductive proofs, understanding of passage to the limit in infinite domains, study of widening, narrowing, and their duals, absence of tool for the calculational design of abstract semantics, logics, or interpreters by abstraction of a semantics, automation of the design of transformers, exploitation of parallelism in fixpoint computations (asynchronous iterations), necessary non-monotony of widening, separation, modularity, analysis of complex data structures, absence of precise specification of libraries, absence of education in static analysis, incompetence of programmers in the use of static analyzers, explainability, hesitation of hierarchies in front of innovation, short terms goals, ignorance of safety and security, belief that artificial intelligence will solve all problems, proliferation of ad-hoc unprincipled research, deficiencies of reviewers in conferences if not journals, to cite a few.

Floating-point arithmetic is counter-intuitive due to inherent rounding errors that potentially occur at every arithmetic operation. A selection of automated tools now exists to ensure correctness of floating-point programs by computing guaranteed bounds on rounding errors at the end of a computation, but these tools effectively consider only straight-line programs over scalar variables. Much of numerical codes, however, use data structures such as lists, arrays or matrices and loops over these. To analyze such programs today, all data structure operations need to be unrolled, manually or by the analyzer, reducing the analysis to straight-line code, ultimately limiting the analyzers’ scalability. We present the first rounding error analysis for numerical programs written over vectors and matrices that leverages the data structure information to speed up the analysis. We facilitate this with our functional domain-specific input language that we design based on a new set of numerical benchmarks that we collect from a variety of domains. Our DSL explicitly carries semantic information that is useful for avoiding duplicate and thus unnecessary analysis steps, as well as enabling abstractions for further speed-ups. Compared to unrolling-based approaches in state-of-the-art tools, our analysis retains adequate accuracy and is able to analyze more benchmarks or is significantly faster, and particularly scales better for larger programs.

This presentation explores theoretical perspectives on static analyses of synchronous data-flow languages, such as Lustre and SCADE, which model programs as sets of equations describing relationships between input and output streams. We discuss the benefits of analyzing the source program directly, rather than compiling away high-level constructs of these languages – such as automata or clocks – and highlight the advantages of using synchronous observers, which allow safety properties to be specified directly as programs. Additionally, we present scheduling techniques that avoid unnecessary computations when solving equations, while preserving the soundness of the semantics.

Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this talk we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. In the talk, we present Path Optimal Symbolic Execution, a novel symbolic execution algorithm that originally accomplishes path optimality against heap-manipulating programs.

The Java type system gives useful guarantees about software, but there are many properties that cannot be expressed. One pervasive property that cannot be expressed is whether a reference can be null or not. The resulting null pointer exceptions are the bane of programmers and have been called the “billion dollar mistake”. They happen even if you think hard about your code and test it thoroughly. There are many causes for null pointer exceptions, including object initialization, missing map keys, confusing contracts, and missing checks. There are many other properties that cannot be expressed in the Java type system that lead to severe runtime errors.

Optional type systems allow developers to improve the quality of their software by encoding additional properties as type systems and enforcing these properties at compile time. We will discuss a type system that prevents null pointer exceptions at compile time and the general framework it builds upon. These optional type systems have found hundreds of bugs in millions of lines of well-tested code. We will discuss alternative tools and interoperability, in particular with Kotlin, and the JSpecify effort to standardize static analysis annotations across the Java ecosystem. Finally, we will briefly discuss whole-program type inference and the interaction of optional type systems with deductive verification.

The development of data science software is prone to a variety of mistakes that can easily compromise the validity of results. While existing tools mainly target low-level programming errors, higher-level issues specific to the data science pipeline remain less systematically addressed.

We present Pyra, a high-level linter designed to detect code smells in data science workflows. Pyra relies on static analysis by abstract interpretation, assigning ad hoc abstract datatypes to program variables and checking their consistency when interacting with data science libraries. By adopting a descriptive type system, Pyra captures suspicious patterns without requiring annotations or code modifications, simply by analyzing Python code.

Pyra currently implements 16 checkers across four categories: misleading visualizations, misleading results (e.g., data leakage), challenges for reproducibility (e.g., missing random seeds), and general issues (e.g., unintended consequences of in-place operations).

By bridging programming and domain-specific best practices, Pyra supports more robust, reproducible, and trustworthy data science pipelines.

Programmers are turning to AI coding assistants to answer questions about their code. Benchmarks are needed to soundly evaluate these systems and understand their performance. To enable such a study, we curate a benchmark of real-world contextualized questions derived from Github pull request comments. Out of this work, we present RubberDuckBench: a multilingual benchmark of questions about code, along with detailed rubrics for evaluating answers. We evaluate a diverse set of 20 LLMs (proprietary & open-source) on answering these questions. We find that even state of the art models fail to give consistent, correct responses across the benchmark. Grok 4 (69.29%), Claude Opus 4 (68.5%), and GPT-5 (67.8%) perform best overall, but do not exhibit pairwise significant superiority over the next 9 best performing models. Most models obtain points through partial credit, with the best performing models only answering at most 2 questions completely correctly across all trials. Furthermore, models often hallucinate with lies in 58.3% of responses on average. Cost analysis reveals no correlation between expense (API pricing or parameter count) and performance. We intend this benchmark to be a target for future research in trustworthy and correct AI coding assistants.

This talk will discuss an enhancement of software bill of materials (SBOMs) with security capabilities to specify and enforce security policies for applications and their software supply chains with the goal of preventing malware.

We present how we do static analysis in Black Duck using Sigma, a fast static analyzer for web/mobile security. We focus on how to make it easier for customers to analyze their code and then understand and prioritize analysis findings. We demo Sigma on an open-source project.

Distributed systems replicate data to improve availability, scalability, and fault tolerance. Ensuring that replicas remain eventually consistent is difficult. Current practices advocate for the use of Replicated Data Types (RDTs) which guarantee convergence out-of-the-box, e.g. CRDTs. However, programming distributed systems using these RDTs is non-trivial due to the lack of appropriate abstractions for replica discovery, update propagation, etc.

In this presentation, we introduce the VeriFx language, a high-level functional object-oriented programming language specially designed to empower developers with automated verification features. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. For each proof, VeriFx derives the necessary proof obligations, which are encoded into first-order logic and discharged automatically by leveraging SMT solving. If a property does not hold, VeriFx returns a high-level counterexample. Verified RDTs can be transpiled to mainstream languages, e.g. Scala. VeriFx provides libraries that implement the execution model and define the correctness properties of well-known RDT families. We used those libraries to verify 51 CRDTs and reproduce a study on the correctness of Operational Transformation functions.

Static program analysis for software bug detection has steadily advanced over many decades and has become a core technology in modern software development. However, the difficulty of inspecting whether analyzer-reported alarms remains a persistent challenge for many developers. In this talk, we present our journey toward addressing this issue and realizing a “fully automated bug detection tool” including buggy input generation. The key lies in “directed input generation”. This technique aims to automatically generate inputs that reach suspicious program points (e.g., static analysis alarms, recently changed code, etc). We will discuss how we combine static analysis with fuzzing and program synthesis to efficiently generate bug-triggering inputs for such points. Also, we share the remaining challenges to improve the current state-of-the-art.

We presented and demoed the Static Analysis and Verification functionality currently supported within the Ciao playground (https://play.ciao-lang.org). The playground is a browser-based program development environment which integrates the CiaoPP abstract interpreter and verifier as an embedded tool. In contrast with the more traditional ways of using CiaoPP (within Visual Studio Code, Emacs, etc.), the playground does not require any installation, while retaining almost all the capabilities of the full, native version of the systems involved. This makes is a very convenient tool for experimentation and teaching. The whole system runs locally on the student’s browser, compiled to web assembly code, and does not need any server infrastructure. This has advantages from the point of view of scalability, low maintenance cost, security, privacy, etc. We presented the playground in action, in different analysis and verification including interactive, on-the-fly, assertion checking as the program is developed, covering properties such as types/shapes, sharing/aliasing, numeric properties, determinism, data sizes, computational cost, etc. We also showed the different configuration options available and the different kinds of information that can be obtained from the analyzer. We demonstrated as well the abstract debugger, that allows advancing step by step in the source program editor while watching the evolution of the abstract values as the fixpoints are computed. Finally, we presented how documents with embedded instances of the analyzer can also be developed within the playground, which allows easily developing interactive tutorials for static analysis tasks, from analyzing and verifying programs to developing new abstract domains.

In this talk, I will introduce an issue in the current trend of developing static analysis techniques and present an efficient approach to address it. To develop cost-effective static analyzers, various static analysis techniques have been proposed. For optimal performance, these techniques should be combined to leverage the benefits of each approach. In the literature, however, the techniques have largely been developed independently, without considering their potential combinations. We discovered that combining independently developed static analysis techniques often results in suboptimal performance, even when each technique is individually optimal. However, developing combinations of techniques while accounting for all interactions between them is a huge burden. To address this issue, I introduce an approach that safely and effectively reduces the burden of developing such combinations.

Mixed-precision tuning is a key optimization technique for numerical programs, where some variables and operations are assigned lower precisions to improve overall performance. It is particularly relevant in applications with frequent numerical computation on resource-constrained hardware, such as embedded systems, scientific computing, and machine learning. The main challenge lies in the trade-off: while reduced precision improves efficiency, it introduces rounding errors that can compromise accuracy.

In this work, we present the first comprehensive evaluation of state-of-the-art tools for mixed-precision tuning. These tools typically fall into two categories: sound static analyses, which offer formal guarantees but are often considered overly conservative, and dynamic methods, which explore a broader optimization space but can violate error bounds, sometimes by several orders of magnitude. Through an extensive comparison on the FPBench benchmark suite, we quantify the trade-offs between performance and soundness. Our results show that sound tools, when enhanced with techniques such as regime inference, can match or even outperform dynamic ones, while still preserving correctness guarantees.

Yet, extending sound guarantees to larger, real-world programs remains a challenge. A promising direction could be to combine static analyses with heuristic guidance – potentially informed by large language models that can help navigate the search space – to improve scalability and enable integration into real-world software engineering workflows.

Decision Trees are a popular kind of predictive models used in machine learning. Previous work in explainable AI by Hurault and Marques-Silva proposed logic-based criteria and algorithms to provide local explanations for model decisions (so-called abductive and contrastive explanations), but efficient explanation synthesis requires models to be stable, a global property difficult to check. In this work, we develop an interval-based method able to formally prove (small-scale) decision tree models to be stable. When they are not stable, we are able to generate counter-examples, compute a quantitative measure of stability, and even provide fixes to make the model stable. We also consider monotony, a more restrictive property than stability, and prove formally monotony as well as infer, when possible, all orders that make the model monotone. We present preliminary experimental results on a few small (4-7 features, 50KB-2MB model size) models trained using Gradient Boosting with XGBoost and LightGBM, from data from OpenML, Kaggle, and UC Irvine. Our preliminary results indicate that, even though the training algorithms are advertised as computing monotone models, the output is not always monotone, and not even stable. In some cases, almost-stable models can be made stable while keeping (or improving) their size and precision. We also show that one-hot encoding is useful to ensure monotony and stability of trained models. This is joint work with Waly Fall.

Static analyzers are complex pieces of software with large dependencies. They can be difficult to install, which hinders adoption and creates barriers for students learning static analysis. This work introduces Try-Mopsa: a scaled-down version of the Mopsa static analysis platform, compiled into JavaScript to run purely as a client-side application in web browsers. Try-Mopsa provides a responsive interface that works on both desktop and mobile devices. Try-Mopsa features all the core components of Mopsa. In particular, it supports relational numerical domains. We present the interface, changes and adaptations required to have a pure JavaScript version of Mopsa. We envision Try-Mopsa as a convenient platform for onboarding or teaching purposes.

The Solana Certora Prover (SCP) is a formal verification tool designed to check the correctness of Solana smart contracts. SCP takes as input both a Solana program and its specification, both written in Rust, and determines whether the implementation satisfies its specification.

In this seminar, I will demonstrate how SCP can be applied to prove fundamental correctness properties of a tokenized vault protocol, including solvency, absence of shares dilution, and fee assessment. I will also discuss the main technical challenges involved in generating efficient and sound SMT-based verification conditions, and how Abstract Interpretation techniques are used to address these challenges.

To put sound program analysis at the fingertips of working class developers, we propose a framework for interactive abstract interpretation of multithreaded C code leveraging mixed-flow sensitivity. Abstract interpretation provides sound analysis results, but can be quite costly in general. To achieve quick response times, we incrementalize the analysis infrastructure, including post-processing, without necessitating any modifications to the analysis specifications themselves. The integration of update rules enables precise incremental analysis of intricate program properties – including concurrency deficiencies such as data-races and deadlocks. A prototype of the framework has been implemented in the static analyzer Goblint, and integrated into IDEs leveraging MagpieBridge. We evaluate our implementation w.r.t. the yard sticks of response time and from-scratch-consistency. We provide examples of program development highlighting the usability of our approach. Lastly, we discuss promising new directions along the lines of on-demand precision increases and incremental result refinement as an interaction between the analyzer and a developer, making the analysis not just incremental but interactive.

Modern cloud-native systems are built as polyglot: multiple languages, frameworks, containers, and deployment descriptors. This makes their actual architecture hard to see and even harder to verify against intended blueprints.

This talk presents a static, multi-artifact analysis approach that reconstructs a system’s architecture by mining source code, build files, Dockerfiles, Helm/Kubernetes manifests, API contracts, and developers’ comunication. In particular, the reconstruction enables to detect recurring cloud-native antipatterns such as shared databases or cyclic service dependencies and to have a overview on the system evolution

Static analysis framework plays a crucial role in determining the capabilities of static analysis to adapt and integrate with modern software engineering practices. Recognizing the limitations of existing frameworks, we have developed Tai-e, a new static analysis framework for Java, aimed at meeting the demands of contemporary software development. Our study shows that Tai-e is easier to learn and use, offering a more extensible and efficient pointer analysis system than other frameworks. This provides a solid foundation for the development and integration of new analysis techniques.

A distinctive feature of modern software engineering today is the reliance on various frameworks, such as microservice, database, and mobile frameworks, rather than building software from scratch. While these frameworks greatly enhance productivity, their complexity poses challenges to the soundness of static analysis. To address this, we leveraged Tai-e’s extensible pointer analysis system to develop a series of innovative techniques and tools for effectively analyzing these framework-based applications. Our evaluation demonstrates that our techniques achieve significantly better soundness compared to state-of-the-art methods for these types of applications.

In this talk, I will introduce Tai-e and our techniques for analyzing modern framework-based software.

Declarative program analysis has long been a powerful tool for detecting data races, tracking information flows, and uncovering security vulnerabilities such as side-channel leaks. However, designing analysis rules that are both accurate and efficient remains a significant challenge, even for domain experts. To improve scalability, many prior works favor efficiency by relaxing completeness, leading to rules that are sound but incomplete. While this trade-off improves performance, it also produces a flood of false alarms, overwhelming developers and reducing the practical usefulness of the analysis.

In this talk, I will present our approach to bridging qualitative and quantitative program analysis. Rather than simply reporting whether a potential issue exists, our framework estimates the probability that a reported issue – such as an information leak – corresponds to a real vulnerability. This probabilistic perspective enables the analysis to prioritize high-risk findings and significantly reduce false alarms. Our solution is built on probabilistic logic programming, extending the widely used Soufflé Datalog engine. I will demonstrate how this framework achieves efficiency, accuracy, and incremental adaptability, making it well-suited for evolving codebases and complex analysis domains.

Discussion Leader: Roberto Bagnara, University of Parma

Discussion Leader: Greta Dolcetti, Ca’ Foscari University of Venice

The adoption of Large Language Models (LLMs) and static analysis together is reshaping how developers interact with code analysis tools [1]. This emerging field offers compelling opportunities to enhance verification workflows, democratize complex analysis techniques, and bridge the gap between technical analysis outputs and developer understanding.

Our discussion group explored how to enhance the developer and user experience through natural language and how hybrid approaches can combine the strengths of these two areas.

Discussion Leader: Michael Schwarz, National University of Singapore

Currently, abstract interpretation is often used only after a program has been developed. However, performing static analysis during development could provide significant benefits, ranging from easing development to detecting bugs much earlier or even preventing them altogether.

Our discussion group explored how to “shift left” abstract interpretation, the prerequisites for doing so, and promising future directions. One of the identified key prerequisites is to make abstract interpreters incremental, i.e., able to efficiently re-analyze a program after small changes. While there is existing work [3, 1, 2, 4], new execution models prevalent in, e.g., data science notebooks pose novel incremental analysis problems, as the effects of previous versions may linger in the environment. This poses challenges at all levels, ranging from defining a version-aware concrete semantics to designing suitable abstract domains. We also discussed why it may be an advantage to maintain results for several old program versions: It may help recover precision if a catastrophic loss of precision occurs for an intermediate version, or allow an incremental analysis to start from the version most semantically similar to the one to be analyzed. We also observed a relationship between incremental analysis and relational analyses relating multiple program versions. It may, for instance, be helpful to alert a user if, after a change intended to be purely cosmetic, the equivalence of the old and new versions can no longer be established.

Beyond incremental analysis, we discussed how to involve developers more directly in the analysis process. For example, they could supply candidate invariants during development. While one may not want to take such invariants at face value, they can guide the analysis in a sound way, e.g., by acting as widening thresholds [5]. Furthermore, it may be useful to provide immediate feedback to developers, e.g., when a call to a function is the first one for which the analysis cannot prove that the argument is non-null, or when a function argument has a value far outside the range of previous calls. While such situations may not be bugs in themselves, they can serve as useful hints to the programmer that something may be amiss and may help avoid the introduction of bugs in the first place. Similarly, the analysis may flag instances where precision degrades significantly, prompting the user to write code more amenable to static analysis and thus likely also easier for humans to understand. Such interactions may help shape code in a way similar to style guides, except that they are tied to a more semantic property, namely whether the analyzer can reason about the code precisely.

We also discussed designing a specification language for developers to express their own properties of interest. To reach widespread adoption, such a specification language may follow the example of the popular semantic patching tool Coccinelle [6] by leveraging familiar syntax to lower the barrier to entry, perhaps by building on existing mechanisms such as CodeQL [7].

One challenge facing work on left-shifting abstract interpretation is the question of how to evaluate such techniques, especially when they involve interactions with users. We concluded that such evaluations may have to involve user studies, which can perhaps best be conducted by collaborating with other communities, such as the HCI community, as few researchers have experience both in sound static analysis and in conducting user studies.