Pour son prochain séminaire l’équipe Cosynus aura le plaisir d’accueillir Constantin Enea pour son exposé intitulé «Specifying and Verifying Consistency Properties».
Résumé: Modern software is typically built with specialized concurrent or distributed objects, which encapsulate shared-memory accesses or message-passing protocols into higher-level abstract data types. These objects are designed to behave according to certain consistency criteria like linearizability, eventual or causal consistency. In this talk, I will give an overview of my recent contributions concerning formal reasoning about concurrent or distributed objects, from efficient testing algorithms to algorithmic verification methods. These results give rise to alternative specification frameworks to characterize the intended behaviors of such objects, which complement the existing generic formalizations of linearizability and weak consistency.