Talk: Checking Consistency of Event-Driven Traces by Mohamed Faouzi Atig
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.
Short Bio: Mohamed Faouzi Atig is a full professor in computer systems at the Department of Information Technology Uppsala University. He has held academic positions at Uppsala University since 2010 from post-doctoral researcher to senior lecturer (associate professor) and since July 2021 to full professor. He obtained his doctoral degree in Computer Science in June 2010 from the University of Paris Diderot – Paris 7 under the supervision of Ahmed Bouajjani and Tayssir Touili and later received a docent degree (comparable to habilitation) from Uppsala University in March 2017. His research focuses on formal verification, model checking, the verification of infinite-state and concurrent systems, weak memory models, string solving, and automata theory.