IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2015 > Parameterized Verification of Asynchronous Shared-Memory Systems
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Pierre Ganty

martes 24 de marzo de 2015

10:45am Lecture hall 1, level B

Pierre Ganty, Assistant Research Professor, IMDEA Software Institute

Parameterized Verification of Asynchronous Shared-Memory Systems

Abstract:

We study systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem. We consider the cases where leader and contributors are in turn modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use a mix of combinatorial properties of the model and some language-theoretic constructions of independent interest. We will also present preliminary results about the liveness verification problem.