The seminar of the Formal Methods and Verification group at the Université Libre de Bruxelles usually takes place on Friday from 11:00 to 12:00 in the room «NO.8.Rotule», campus Plaine (show route), and can be accessed remotely via Zoom.

To get informed of current and future seminar via our mailing list (and get the Zoom link), please contact debraj chakraborty ulb ac be or subscribe here, or to our seminar calendar.

Talks in 2022-23

27/01/202311hRotuleWen-Chi Yang (KULeuven)TBATBA
08/12/202211hRotuleLouise Sadoine (UMONS)Towards decentralized Models for day-ahead scheduling of energy resources in Renewable Energy CommunitiesRenewable energy communities (RECs) are one of the driving factors for ensuring the energy transition. These consist in decentralized market mechanisms enabling local electricity exchanges among end-users, and bypass the traditional wholesale/retail market structure. In this configuration, local consumers and prosumers (i.e., consumers who also produce electricity) join together in collectives, known as communities. They can either cooperate or compete to achieve a (possibly common) goal, which may be economic, environmental, or social. We address electricity consumption scheduling on a day-ahead basis within a community of prosumers that own renewable generation. To this end, we mobilize prosumer flexibility to optimize energy exchanges based on the desired objective (e.g. the electricity bill).

First, we establish a typology of community market designs that enable virtuous coordination between members. Among them, we design different centralized and decentralized schemes. In the former, a centralized planner globally optimizes the common objective, while in the latter, each member optimizes its consumption based on its energy preferences. We, therefore, place particular emphasis on modeling strategic behavior. The natural interdependence between members sharing a common network, reflected by an aggregate network tariff component, leads to the formulation of non-cooperative games. In addition, excess rooftop solar power production can be valued inside or outside the community.

We analyze the existence, uniqueness, and computation of Nash equilibria. We use distributed algorithms that ensure confidentiality and do not require third-party intervention. For all different models, we evaluate the efficiency of the results and provide insight into their respective incentives.
25 / 11 / 202211hRotuleLéonard Brice (ULB)To appearTo appear
10 / 11 / 202211hRotuleMrudula Balachander (ULB)LTL Reactive Synthesis with a Few HintsWe study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against a hostile environment. In the variant studied here, the user provides the high level LTL specification φ of the system to design, and a set E of examples of executions that the solution must produce. Our synthesis algorithm works in two phases. First, it generalizes the decisions taken along the examples E using tailored extensions of automata learning algorithms. This phase generalizes the user-provided examples in E while preserving realizability of φ. Second, the algorithm turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine that realizes φ. The examples are used to guide the synthesis procedure. We provide a completness result that shows that our procedure can learn any Mealy machine M that realizes φ with a small (polynomial) set of examples. We also show that our problem, that generalizes the classical LTL synthesis problem (i.e. when E = ∅), matches its worst-case complexity. The additional cost of learning from E is even polynomial in the size of E and in the size of a symbolic representation of solutions that realize φ. This symbolic representation is computed by the synthesis algorithm implemented in Acacia-Bonzai when solving the plain LTL synthesis problem. We illustrate the practical interest of our approach on a set of examples.
14/10/202211hRotulePierre Vandenhove (UMONS)Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite GraphsWe consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of ω-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is ω-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be ω-regular. This provides a game-theoretic characterization of ω-regular objectives, and this characterization can help in obtaining memory bounds. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs. We illustrate our results with the family of discounted-sum objectives, for which ω-regularity depends on the value of some parameters.
21/10/202211hRotuleGaëtan Staquet (UMONS)Learning Realtime One-Counter AutomataWe present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.
30/09/202211hRotuleAntonio Paolillo (Huawei)Enabling Performance on Concurrent Modern Hardware with Practical Verification Modern commodity hardware is very diverse.
On many-core servers, different core pairs within the same processor may communicate with different speeds due to deep memory hierarchies (caches, NUMA memory, etc.).
On embedded systems, groups of cores can have different processing and energy consumption specifications (e.g. big.LITTLE architectures).
Moreover, on some architectures, memory operations can be reordered in a multitude of ways.

To build efficient systems, software designers cannot treat cores as homogeneous, freely exchangable processing units.
Algorithms, specially concurrent algorithms, have to be aware of the hardware heterogeneity to be able to exploit it.
Unfortunately, awareness has an intrinsic cost: complexity.

In this talk, we argue that some level of formal verification is a requisite for system builders willing to take the next step in the design of concurrent algorithms.
Without that, systems are doomed to fail in the most unpredictable and unreproducible ways.
We review and connect a few of our success stories and draw a path for the future work."
02/09/202211hRotuleFrank Cassez (ConsenSys Software R&D)Deductive Verification of Smart Contracts with DafnyWe present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary reentrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.

Joint work with Joanne Fuller and Horacio Mijail Ant´on Quiles
Link to paper:

Past Talks

Edwin Hamel-De le Court (ULB)

Two-Player Boundedness Counter Games

Ayrat Khalimov (ULB)

Recent Developments in Register-Bounded Synthesis

Benedikt Maderbacher (IAIK, TU Graz)

Reactive Synthesis modulo Theories

Amazigh Amrane (Rouen Normandy University)

Logic and Rational Languages of Scattered and Countable Series-Parallel Posets

Sayan Mukherjee (Chennai Mathematical Institute)

Reachability in Timed Automata with Diagonal Constraints and Updates

Anirban Majumdar (LSV & INRIA Rennes)

Parameterized Concurrent Games

Chana Weil-Kennedy (TU Munich)

Verification of Immediate Observation Petri Nets

Léo Henry (IRISA)

Active learning of timed automata with unobservable resets

Edwin Hamel (IRIF)

An algebraic theory for state complexity

Clément Tamines (University of Mons)

Stackelberg-Pareto Synthesis

Léonard Brice (ULB)

Subgame-perfect equilibria in mean-payoff games

Sarah Winter (ULB)

Synthesizing computable functions from synchronous specifications

Satya Prakash Nayak (Chennai Mathematical Institute)

Robust Linear Temporal Logics

Debraj Chakraborty (ULB)

Monte Carlo Tree Search guided by Symbolic Advice for MDPs

Raphaël Berthon (ULB & University of Antwerp)

Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

Léo Exibard (ULB & Aix-Marseille Université)

Computability and Continuity of Data Word Functions Defined by Transducers

Ayrat Khalimov (ULB)

Church Synthesis on Register Automata over Infinite Ordered Domains

Older archives