IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2015 > Parameterized Verification of Asynchronous Shared-Memory Systems

Pierre Ganty

Tuesday, March 24, 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.