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.

CFL replaces this approach with a powerful DFS-like algorithm inspired by fuzzing. This feedback is used to construct schedulers that guide model exploration, enabling both a richer variety of states for invariant generation and 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. This talk proposes a novel method for validating concurrent correctness witnesses based on thread-modular abstract interpretation, using ghost variables to guide the exploration of thread interleavings.

In-progress research — joint work with Zhendong Ang and Umang Mathur.

This talk introduces oriented metrics — asymmetric distance measures on programs — to structure search spaces in syntax-guided synthesis. Four reduction techniques are presented: pruning, factorization, abstraction/refinement, and improved enumeration. A new generic solver built on these techniques consistently outperforms the state of the art by more than an order of magnitude on string and bitvector benchmarks.

This talk presents Leslie, a Lean-based verification environment for distributed protocols. Leslie proofs can be automatically generated by LLM agents, even on classical examples where model checking techniques struggle — raising the question: is the era of model checking over?

Malware is growing at an extraordinary pace, making efficient detection critical. Existing antivirus systems rely on code emulation or signature matching, but both approaches have significant limitations. This talk presents a static approach based on behavioral signatures that checks program behavior without execution.

The technique was implemented and tested against several viruses, detecting over 800 — including many missed by Avira, Avast, Norton, Kaspersky, and McAfee.

This paper addresses reachability in concurrent programs with an arbitrary number of threads under the eTSO model for Intel x86. While prior work established decidability under k-alternation bounding for a fixed number of threads, this paper proves decidability in the parametrized setting — where the thread count is unbounded.

The key difficulty is overcome via a novel reduction to reachability in well-structured systems over BQO (Better Quasi Order) domains — the first such use of BQO-based well-structured systems for infinite-state program verification.

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

Online services built on scalable microservice architectures must be updated on the fly without interrupting operation. This paper introduces a framework formalizing atomic update consistency and derives the first algorithms guaranteeing consistency for mixed-mode updates, leveraging semantic properties such as commutativity.

Geo-replicated systems achieve low latency and high availability by letting nearby replicas serve updates concurrently, but reconciling those updates without violating application invariants is hard. This talk presents a general coordination-free approach combining replicated data types with application-defined conflict-resolution policies, enabling convergence while preserving safety properties such as uniqueness and bounded resources.

A new class of simulation relations is introduced for compositional reasoning about randomized distributed protocols, preserving a wide range of properties from LTL to branching and probabilistic trace distributions. The technique is demonstrated on a non-trivial randomized protocol for Byzantine Agreement.

Formal verification tools typically assume public formulas — problematic when specifications encode sensitive information. This talk surveys work on privacy-preserving automated reasoning, integrating cryptographic techniques into verification workflows.

It also presents Crepe, the first zero-knowledge proof system targeting a PSPACE-complete problem: regular expression equivalence. Based on regex derivatives and coinductive reasoning, Crepe validates hundreds of large equivalence proofs in seconds.

This talk examines two verification techniques — bounded model checking (BMC) and counterexample-guided abstraction refinement (CEGAR) — exploring directions for partially integrating aspects of each into the other, along with resulting findings and open research questions.

This work introduces natural reductions, an expressive syntactic class of reductions for parameterized concurrent programs, and studies the complexity of deciding their soundness. Without thread synchronization, a polynomial-time algorithm is presented. With synchronization, the problem is shown to be coNP-hard even for simple mechanisms such as locking.