Albert Atserias

Universitat Politècnica de Catalunya, Spain

Local-vs-Global Consistency of Annotated Relations

In modern relational database theory, annotated relations constitute an expressive formal extension of the classical framework to model a large variety of problems. When the tuples of the relations come annotated with values from the tropical semiring, annotated relations can be used to model reachability and shortest paths problems on weighted graphs and cost optimization problems. When the tuples come annotated with positive real numbers, annotated relations can be used to model statistical data and its associated data analysis problems. A third, very different, example is that of relations whose tuples come annotated with positive linear operators of a Hilbert space, which can be used to model the joint measurability problem in quantum mechanical systems.

A fundamental challenge in each of these fields is determining the necessary and sufficient conditions under which local components given by local annotated relations admit a global realization as a single annotated relation that projects to the local constituents. This is an instance of the local-vs-global consistency problem for annotated relations. After reviewing the formal framework of K-relations, where K is a positive commutative semiring or monoid and each tuple in each relation comes annotated with a value from K, we adapt the standard notions of consistency for classical relations to the setting of K-relations. We highlight both the parallels with the classical framework of standard relations and the key differences that make this theory particularly rich and interesting.

Alastair F. Donaldson

Imperial College London, UK

When You Have a Fuzzer, Everything Looks Like a Reachability Problem

We provide an overview of three projects that explore the idea of using coverage-guided fuzzing, a technique traditionally used for finding bugs in software, in unconventional domains:

• ●  efficiently solving SMT formulas that use floating-point constraints;
• ●  achieving fast SMT sampling for such formulas;
• ●  simulating operational memory models.

In each case, the idea is to reduce the problem at hand into a reachability problem: transforming a problem instance into a program equipped with a special error location, such that finding an input that reaches the error location equates to finding a solution to the problem instance. Coverage-guided fuzzing, which excels at mutating a corpus of inputs to achieve increasing statement coverage of a system under test, can then be used to search for an input that reaches the error location—i.e., for a solution to the problem instance. We hope this overview will inspire other researchers to consider recasting search problems into a reachability problem form where coverage-guided fuzzing may prove effective.

Zak Kincaid

Princeton University, US

Reachability problems and program analysis

Since essentially all decision problems concerning the semantics of computer programs are undecidable, the goal in program analysis is to compute approximate semantics. While approximation heuristics are often effective in practice, they can also be brittle and unpredictable. In this talk, I will summarize a line of work that aims to create more robust program analyses by exploiting reachability techniques for sub-Turing models of computation.

Anthony W. Lin

University of Kaiserslautern, Germany

The Role of Logic and Automata in Understanding Transformers

The advent of transformers has in recent years led to powerful and revolutionary Large Language Models (LLMs). Despite this, our understanding on the capability of transformers is still meager. In this invited talk, we recount the rapid progress in the last few years to the question of what transformers can do. In particular, we will see the integral role of logic and automata (also with some help from circuit complexity) in answering this question. We also mention several open problems at the intersection of logic, automata, verification and transformers.

Mickael Randour

Université de Mons, Belgium

Simplicity Lies in the Eye of the Beholder: A Strategic Perspective on Controllers in Reactive Synthesis

In the game-theoretic approach to controller synthesis, we model the interaction between a system to be controlled and its environment as a game between these entities, and we seek an appropriate (e.g., winning or optimal) strategy for the system. This strategy then serves as a formal blueprint for a real-world controller. A common belief is that simple (e.g., using limited memory) strategies are better: corresponding controllers are easier to conceive and understand, and cheaper to produce and maintain.

This invited talk focuses on the complexity of strategies in a variety of synthesis contexts. We discuss recent results concerning memory and randomness, and take a brief look at what lies beyond our traditional notions of complexity for strategies.

Niki Vazou

IMDEA Software Institute, Madrid

LiquidHaskell: Theorem Proving with Refinement Types

Liquid Haskell is an extension to Haskell that adds refinement types to the language, which are then checked via an external theorem prover such as z3. With refinement types, one can express many interesting properties of programs that are normally out of reach of Haskell's type system or only achievable via quite substantial encoding efforts and advanced type system constructs. On the other hand, the overhead for checking refinement types is often rather small, because the external solver is quite powerful.

Liquid Haskell used to be an external, standalone executable, but is now available as a GHC plugin, making it much more convenient to use.

In this tutorial, we'll discuss how refinement types work, give many examples of their use and learn how to work with Liquid Haskell productively.