logo

Logic Seminar

Organizers: Laurențiu Leuștean, Andrei Sipoș


The logic seminar features talks on
mathematical logic,
philosophical logic and
logical aspects of computer science.
All seminars, except where otherwise indicated,
will be at 10:00 in Hall 202,
Faculty of Mathematics and Computer Science,
University of Bucharest.
logo
Past Seminars

    Our logo and our posters are designed by Claudia Chiriță.


Talks in 2019-2020


Thursday, September 19, 2019 in Hall 214

Radu Iosif (CNRS - VERIMAG, France) )
Checking Deadlock Freedom of Component-based Systems


Abstract: We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology (i.e. architecture) of the system (e.g. pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
Joint work with Marius Bozga and Joseph Sifakis.


    Past Seminars