The verification of concurrent systems with potentially infinite state spaces remains a recurring challenge in formal verification. One way to address this problem is through symbolic techniques that explore representations of sets of states rather than individual executions. In this seminar, we present a narrowing-based approach to the symbolic verification of concurrent systems specified as rewrite theories in Maude. We first introduce the main ideas behind symbolic reachability analysis, constrained narrowing, and folding techniques, showing how they can be used to explore infinite-state systems. The main focus of the seminar is DM-Check, a deductive model checker that combines narrowing-based symbolic exploration with the inductive theorem proving capabilities of NuITP. Through two representative case studies, we illustrate how DM-Check supports the semi-automated verification and generation of inductive invariants, enabling users to establish safety properties that would be difficult to verify through direct state-space exploration alone. Finally, we discuss current challenges and possible directions for future research.

Systems that interact synchronously with an unpredictable environment are usually captured by zero-sum concurrent games. In such games, randomised strategies are in general more powerful than deterministic ones. Such systems, however, do not capture faithfully decentralised systems that cannot resort to a common private source of randomness. In this talk, I will introduce dicey games, a model for games played by teams, where the structure of randomness sources accessible to each player is explicitly specified.

Approximate nearest neighbour (ANN) search is central to modern data-intensive applications, particularly on large-scale, heterogeneous, or high-dimensional datasets. However, many existing ANN methods struggle in such scenarios, either because they rely on metric assumptions or because their indexing strategies are ill-suited to distributed environments or memory-constrained settings. This talk introduces PDASC (Parametrizable Distributed Approximate Similarity Search with Clustering), a distributed ANN search algorithm whose index design addresses three common concerns in ANN search: supporting arbitrary dissimilarity functions, native distributed execution, and efficient operation under constrained memory environments.

We transport multi-stage programming from functional to relational programming, with novel constructs to give programmers control over staging and non-determinism. We stage interpreters written as relations, in which the programs under interpretation can contain holes representing unknown expressions or values. By compiling the known parts without interpretive overhead and deferring interpretation to run time only for the unknown parts, we compound the benefits of staging (e.g., turning interpreters into compilers) and relational interpretation (e.g., turning functions into relations and synthesizing from sketches). We extend miniKanren with staging constructs and apply the resulting multi-stage language to relational interpreters for subsets of Racket and miniKanren as well as a relational recognizer for context-free grammars. We demonstrate significant performance gains across multiple synthesis problems, systematically comparing unstaged and staged computation, as well as indicatively comparing with an existing hand-tuned relational interpreter.

Smart contracts deployed on blockchain platforms are immutable and control billions of dollars in assets, making their correctness paramount. This dissertation strengthens the Solidity ecosystem through empirically- grounded investigation and feedback-driven tool development. We present the first large-scale mixed-methods study of Solidity’s language design, an- alyzing 296,000 smart contracts, surveying 31 developers, and evaluating 11 analysis tools. Our findings reveal that existing tools detect only 43.5% of error-handling misuses and that documentation instability discourages developer consultation. Building on these findings, we introduce FUZ- ZOL, a syntax-aware mutation fuzzer that discovered 19 compiler bugs (17 fixed), achieving up to 5.8× higher coverage than state-of-the-art fuzzers. We also introduce DGRed, which reduces deployment gas costs by 15.65% through search-based state variable mutation, challenging conventional vari- able packing practices.