Keynote talk I

I- Parameterized Verification of Asynchronous Shared-Memory Systems“.

Esparza Javier Esparza
Technical University of Munich, Germany

Biography of Javier Esparza:
Javier Esparza holds the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technische Universität München since 2007. Previously he held the Chair of Software Reliability and Security at the University of Stuttgart (2003-2007), the Chair of Theoretical Computer Science at the University of Edinburgh (2001-2003), and worked as Associate Professor at the Technische Universität München (1994-2001). He has co-authored a book on Free Choice Petri nets with Jörg Desel, and a book on the unfolding approach to Model Checking with Keijo Heljanko. He has published over 130 scientific papers in the fields of automatic program verification, program analysis, concurrency theory, and automata theory. Javier Esparza has contributed to the theory Petri nets, and was one of the initiators of the unfolding approach to model checking, the automata-theoretic approach to software model checking, and the verification of infinite-state systems. More recently he has conducted research on the fundamentals of program analysis and the verification of parametrized and stochastic systems. His group has developed several verification tools, including Moped and jMoped and Rabinizer. Javier Esparza received a honorary doctorate in Informatics from the Masaryk University of Brno in 2009 and is member of Academia Europaea since 2011.

We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. There is no synchronization primitive to execute a sequence of operations atomically. The model is inspired by distributed algorithms implemented on sensor networks. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use combinatorial characterizations of computations in the model, and in the case of pushdown systems, some novel language-theoretic constructions of independent interest.
This is joint work with Pierre Ganty and Rupak Majumdar.

Dates [No Extensions]

January 9, 2015

Abstract submission deadline

January 18, 2015

Paper submission deadline

March 16, 2015

Acceptance notification

April 13, 2015

Camera ready copy due



The proceedings of the conference will be published in Springer’s Lecture Notes in Computer Science