Mohamed Faouzi Atig, UPPSALA University

Professor in computer systems at the Department of Information Technology, Uppsala University. its research interests broadly span model checking, verification of infinite-state systems, weak memory models, and automata theory.

Abstract: We study the consistency checking problem, which consists in determining whether, for a given program and a trace (e.g., an execution graph), there exists an execution of the program that satisfies all the relations of the trace. This problem has been widely explored for various programming models In this work, we focus on event-driven programs, which extend concurrent shared-memory programs by allowing threads—called handlers—to send and receive messages. Each handler has a mailbox for incoming messages, which are processed sequentially. However, message executions of different handlers may interleave. We propose an equivalent axiomatic model for event-driven programs and analyze the complexity of their consistency checking problem.

Sylvain Conchon, Paris-Saclay University

Professor at Paris-Saclay University and a member of LMF (the Formal Methods Laboratory - ULMR 9061) and the Toccata team, a joint project with INRIA Saclay - Île-de-France. Previously, He was Senior Research Associate in the OBASCO team at Ecole des Mines de Nantes, Senior Research Associate in the PacSoft team at the OGI School of Science & Engineering at OHSU and Ph.D student at INRIA Rocquencourt in the MOCSOVA team

The Cubicle Fuzzy Loop : A Fuzzing-Based Framework for the Cubicle Model Checkler
Abstract: This talk presents the Cubicle Fuzzy Loop (CFL), a fuzzing-based extension for Cubicle, a model checker for parameterized systems. To prove safety, Cubicle generates invariants, making use of forward exploration strategies like BFS or DFS on finite model instances. However, these standard algorithms are quickly faced with the state explosion problem due to Cubicle’s purely nondeterministic semantics. This causes them to struggle at discovering critical states, hindering 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 used by CFL to construct schedulers that guide the model exploration. Not only does this provide Cubicle with a bigger variety of states for generating invariants, it also quickly identifies unsafe models. As a bonus, it adds testing capabilities to Cubicle, such as the ability to detect deadlocks. Our first experiments have yielded promising results. CFL effectively allows Cubicle to generate crucial invariants, useful to handle hierarchical systems, while also being able to trap bad states and deadlocks in hard-to-reach areas of such models.