Workshop Program

This talk presents the Cubicle Fuzzy Loop (CFL), a fuzzing-based extension of Cubicle, a model checker for parameterized systems. To prove safety, Cubicle generates invariants using forward exploration strategies such as BFS or DFS on finite model instances. However, these standard algorithms quickly face the state explosion problem due to Cubicle's purely nondeterministic semantics. As a result, they struggle to discover critical states, which hinders invariant generation.

CFL replaces this approach with a powerful DFS-like algorithm inspired by fuzzing. Cubicle's purely nondeterministic execution loop is modified to provide feedback on newly discovered states and visited transitions. This feedback is then used by CFL to construct schedulers that guide model exploration. Not only does this provide Cubicle with a richer variety of states for invariant generation, but it also enables the rapid detection of unsafe models.

Our first experiments have yielded promising results. CFL effectively enables Cubicle to generate crucial invariants for hierarchical systems.

Concurrent programs are difficult to verify, and even sound verification tools sometimes produce incorrect results due to implementation bugs. Correctness witnesses have been proposed to increase confidence in verification results, and have recently been extended to concurrent programs using ghost variables to encode expressive invariants. However, techniques for validating such witnesses remain underdeveloped.

In this talk, we propose a novel method for validating concurrent correctness witnesses based on thread-modular abstract interpretation. Our key idea is to use ghost variables from the witness to guide the exploration of thread interleavings. This allows the analysis to verify witnesses with invariants beyond the reach of standard thread-modular approaches, while retaining the scalability benefits of thread-modular abstract interpretation.

This in-progress research is joint work with Zhendong Ang and Umang Mathur.

In syntax-guided synthesis, one of the challenges is to reduce the enormous size of the search space. We observe that most search spaces are not just flat sets of programs, but can be endowed with a structure that we call an oriented metric. Oriented metrics measure the distance between programs, like ordinary metrics do, but are designed for settings in which operations have an orientation. Our focus is on the string and the bitvector domains, where operations like concatenation and bitwise conjunction transform an input into an output in a way that is not symmetric. We develop several new oriented metrics for these domains.

Oriented metrics are designed for search space reduction, and we present four techniques: (i) pruning the search space to a ball around the ground truth, (ii) factorizing the search space by an equivalence that is induced by the oriented metric, (iii) abstracting the oriented metric (and hence the equivalence) and refining it, and (iv) improving the enumeration order by learning from abstract information. We acknowledge that these techniques are inspired by developments in the literature. By understanding their roots in oriented metrics, we can substantially increase their applicability and efficiency. We have integrated these techniques into a new synthesis algorithm and implemented the algorithm in a new solver. Notably, our solver is generic in the oriented metric over which it computes. We conducted experiments in the string and the bitvector domains, and consistently improve the performance over the state-of-the-art by more than an order of magnitude.

I will talk about Leslie, a Lean-based verification environment for distributed protocols. I will show that Leslie proofs can be automatically generated by LLM agents, even on classical examples for which model checking techniques struggle. Which brings me to the question: is the era of model checking over?

The number of malware is growing extraordinarily fast. A malware may bring serious damage. Thus, it is crucial to have efficient up-to-date virus detectors. Existing antivirus systems use various detection techniques to identify viruses such as (1) code emulation where the virus is executed in a virtual environment to get detected; or (2) signature detection, where a signature is a pattern of program code that characterizes the virus. A file is declared as a virus if it contains a sequence of binary code instructions that matches one of the known signatures. These techniques are becoming insufficient. Indeed, emulation based techniques can only check the program's behavior in a limited time interval. As for signature based systems, it is very easy for virus developers to get around them. Thus, a robust malware detection technique needs to check the behavior (not the syntax) of the program without executing it.

We show in this talk how using behavior signatures allow to efficiently detect malwares in a completely static way. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.

We address the reachability problem for concurrent programs with an arbitrary number of threads running over the Intel x-86 architecture. We consider the formal model eTSO for Intel x-86 defined by Raad et al. in POPL 2022. This model takes into account multiple memory types and non-temporal writes, combining in a complex way features in the TSO and PSO weak memory models. In PLDI 2024, Abdulla et al. proved that this problem is undecidable for eTSO in general, but that it is decidable under k-alternation bounding when computations have, for some fixed bound k, at most k alternations of TSO segments (with TSO writes only) and PSO segments (with PSO writes only) for each thread. The proof of this result assumes that the number of threads is fixed, and relies crucially on referring to thread identities.

In this paper, we prove the decidability of the k-alternation bounded reachability problem of eTSO in the parametrized setting when the number of threads is a parameter that can be arbitrarily high. The proof is nontrivial as it cannot refer to thread identities, their number being unbounded. We show that it is possible to overcome this difficulty using a novel and quite complex reduction to reachability in well-structured systems on domains that are BQOs (Better Quasi Orders). This is the first time that BQO-based well-structured systems are used to prove the decidability of verification of infinite state programs.

Joint work with Parosh Aziz Abdulla, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan.

Online services are commonly implemented with a scalable microservice architecture, where isomorphic workers process client requests, recording persistent state in a backend data store. To maintain service, modifications to service functionality must be made on the fly -- i.e., as the service continues to process client requests -- but doing so is challenging. The central difficulty is that of avoiding inconsistencies from mixed-mode operation, caused by workers of current and new versions interacting via the data store. Some update methods avoid mixed-mode altogether, but only at the cost of substantial inefficiency -- by doubling resources (memory and compute), or by halving throughput. The alternative is an uncontrolled "rolling" update, which runs the risk of serious service failures arising from inconsistent mixed-mode behavior.

Ideally, it should appear to every client that a service update takes effect atomically; this ensures that a client is not exposed to inconsistent mixed-mode behavior. In this paper, we introduce a framework that formalizes this intuition and develop foundational theory for reasoning about update consistency. We apply this theory to derive the first algorithms that guarantee consistency for mixed-mode updates. The algorithms rely on semantic properties of service actions, such as commutativity. We show that this is unavoidable, by proving that any semantically oblivious mixed-mode update method must allow inconsistencies.

Geo-replicated systems deliver low latency and high availability by allowing users to access and update nearby replicas. However, when updates execute concurrently at different replicas, the system must reconcile them without violating application-level invariants. The CAP theorem formalises this tension: in the presence of network partitions, systems must trade off between consistency and availability. Adopting weak consistency preserves availability but risks compromising correctness. Replicated data types offer a coordination-free path to convergence, yet they do not account for application invariants, and existing methods for maintaining such invariants typically rely on coordination, sacrificing the very availability and low latency that weak consistency is designed to provide.

This talk presents a general approach to enforcing correctness in weakly consistent replicated systems entirely without coordination. The central idea is to combine replicated data types with application-defined conflict-resolution policies that determine how incompatible concurrent operations are handled. By resolving conflicts locally and deterministically, replicas converge while preserving safety properties such as uniqueness and bounded resources. The talk will discuss the consistency challenges that arise in global-scale systems, the trade-offs between coordination and availability, and how principled, coordination-free conflict resolution can support fast, safe execution across replicas.

We present a technique for compositional reasoning about randomized distributed protocols. The main contribution consists in defining a new class of simulation relations that preserve a wide and heterogenous class of properties ranging from simpler LTL properties to branching properties or properties relating to probabilistic trace distributions. We show the applicability of this technique on a non-trivial randomized protocol solving Byzantine Agreement.

Formal methods provide powerful techniques for proving correctness of software and hardware systems against specifications, and modern tools now scale to industrial applications. However, they typically assume that the formulas being analyzed are public, which is problematic when the specification itself encodes sensitive information.

In this talk, we give an overview of our work on privacy-preserving automated reasoning, where cryptographic techniques are integrated into formal verification workflows to protect both inputs and intermediate reasoning. We describe zero-knowledge protocols for proving unsatisfiability and discuss how standard verification pipelines can be adapted to privacy-sensitive settings.

We will also outline Crepe, a zero-knowledge proof system for regular expression equivalence. Crepe is the first ZK protocol targeting a PSPACE-complete problem and is based on a proof calculus using regular expression derivatives and coinductive reasoning. It includes a sound and complete proof generation procedure and efficiently verifies large equivalence proofs, validating hundreds of instances in a few seconds each.

Verifying a program consists of proving that all its executions satisfy a given specification. Existing verification approaches often focus on particular classes of programs and develop techniques that make analysis practical in those settings. Since these techniques rely on different abstractions and assumptions, an important question is whether concepts from one approach can be incorporated into another, and how such combinations affect the resulting verification process in terms of both expressive power and performance.

This talk considers two examples: bounded model checking (BMC) and counterexample-guided abstraction refinement (CEGAR). I discuss possible directions for partially integrating aspects of one technique into the other, and highlight several results and open research questions that arise from these combinations.

The verification of reductions, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syntactic reductions, which we call natural reductions. Natural reductions are specified by introducing atomic blocks and global rendezvous points in the parameterized program's thread template. We study the problem of deciding whether a given natural reduction is sound wrt. a given (semi-)commutativity relation. In the case that there is no synchronization between threads, we present a sound and complete polynomial-time algorithm. In the case where synchronization is considered, we provide a general lower bound for the problem (parametric in the synchronization mechanism), and show that the problem is coNP-hard already for a simple mechanism like locking.