Invited Speakers of VECoS 2019
Verifying Robusteness of Concurrent Systems
Ahmed Bouajjani, Paris Diderot University
Abstract: Concurrent systems are in general used by their clients under strong assumptions on their visible behaviors. These assumptions allow the adoption of a modular design approach where at the level of the client it is possible to reason abstractly about the behaviors of the invoked systems. For instance, the users of a shared memory may assume that the implementation of the memory is sequentially consistent, i.e., it behaves according to the interleaving model where write/read operations are considered to be atomic and immediately visible to all parallel users. In an another context, the users of web services may consider that their requests are handled atomically in a serial way, etc. However, for performance reasons, the implementations of concurrent systems tend to parallelize operations, and to reorder their execution in order to increase the throughput of the system. This leads to implementations that offer in general relaxed consistency guarantees (compared w.r.t. to strong consistency models). In this talk, we will address the issue of checking that a given client program is robust against this kind of relaxations, i.e., the observable behaviors of the client are the same under both the strong and relaxed consistency models. Robustness ensures the preservation by the considered relaxations of all properties that can be proved under strong consistency. We show that this property can be checked efficiently in several cases by linear reductions to state reachability problems under the strong semantics, which allows to obtain a significant gain in the complexity.
Short Bio: Ahmed Bouajjani got a PhD and a Habilitation in CS from the Univ. of Grenoble (1990, 1999). He was associate professor at the Univ. of Grenoble/Verimag lab. (1990-99), in leave at CNRS from 1994 to 1996. He is professor at Paris Diderot U./LIAFA-IRIF lab. since 1999. He is senior member of the "Institut Universitaire de France" since 2013. He got a "Carl Friedrich von Siemens Research Award of the Alexander von Humboldt Foundation" in 2018. He is the head of the "Automata, Structures, and Verification" pole of the IRIF lab. since 2017. He has been the head of the "Modelling and Verification" team in 2004-2017. He is in the IRIF direction board and deputy director of the doctoral school of « Math. Sci. of Paris Center ». He co-chaired the PC’s of 5 intern. conferences, he is in the editorial boards of 2 journals, in the SC of 2 conferences, and was in the CAV Award Committee (2013-16). He was visiting professor at TU Munich, U. Uppsala, Chennai Math. Inst., Microsoft Research, Koç U., etc. He published more than 130 articles. His main research interests are formal methods, program verification, concurrency, infinite-state model-checking algorithms, automata and logics.
1968 to 2019: Half a Century of Correctness Enhancement
Ali Mili, New Jersey Instirtue of Technology (NJIT)
Abstract: Whereas correctness preservation is considered as the gold standard of software engineering processes, in this talk we argue that in fact the vast majority of software engineering processes do not involve correctness preservation but rather correctness enhancement. We explore some mathematics of correctness enhancement, discuss in what way and to what extent correctness correctness enhancement pervades software engineering, and tentatively speculate about prospects for using these insights to enhance software engineering practice.
Short Bio: Ali Mili holds a PhD in CS from the University of Illinois and a Doctorat es-Sciences d'Etat from the University of Grenoble. He served as chairperson of the CS department at the University of Tunis and currently serves as Professor and Associate Dean in the Ying Wu College of Computing at NJIT, Newark, NJ.