Last modified: Sat Apr 21 15:38:10 CEST 2018 Verification of Distributed Systems

Verification of Distributed Systems

May 9--11, 2018
NETYS 2018
Essaouira, Morocco

Context and goal

Modern computer systems rely crucially on concurrency and distribution to meet increasing high performance requirements. The rise of new technologies such as multi-core processors and could-computing have pushed concurrent and distributed programming to the mainstream. However, the development of concurrent and distributed systems that are both performant and consistent is a huge challenge, both from the conceptual and practical viewpoints. Researchers and practitioners in the fields of databases, cloud computing, parallel programming, concurrency, programming languages, and verification have independently tackled this challenge focusing on unique problems arising in their respective domains. We believe that there is significant potential for synergy by bringing together researchers from these diverse areas to build upon insights and techniques from each other. The main goal of this workshop is to provide an opportunity for such a synergy and to foster collaboration between the participants. Participation in the workshop is by invitation only. The workshop follows a tradition of workshops on related topics; see, e.g., FRIDA 2016 held in Marrakech, Morocco, May 17, 2016.

Topics of interest:

A central theme of the workshop will be the issue of correctness in the development of performant concurrent and distributed systems. In this workshop, we would like to explore the different correctness notions that are used in this context and to understand the relationship between them. We would like to investigate methods for specifying, verifying, and testing systems against these notions. Here are some suggested topics that are of interest to this workshop:

Correctness criteria: What forms of consistency notions are appropriate for the different class of concurrent and distributed applications? What abstractions do these correctness criteria offer to the applications? What kinds of correctness properties do applications typically require?
Specification: How do the applications specify the required correctness properties?
Systems: To what degree can these properties be guaranteed by the platform (programming language, libraries, and runtime system)? What are the performance tradeoffs when one moves the responsibility for correctness between the platform and application?
Modularity: Can we build concurrent/distributed systems for which correctness can be established in a modular manner?
Verification: How do we build automatic verification and testing tools that determine if applications ensure the desired specification?
Synthesis: Can program synthesis aid in achieving correct-by-construction applications?

Organizers

Ahmed Bouajjani, Univ Paris Diderot, France
Andreas Podelski, University of Freiburg, Germany

Dates and venue

The workshop will take place in May 9--11. The venue is the same as for NETYS 2018.

Accomodation

See http://netys.net/accommodation/

Program

Sunday May 9

09:00 - 09:15 Opening

09:15 - 10:15 Session 1:

speaker: title
speaker: title

10:15 - 11:00 Break

11:00 - 12:30 Session 2:

speaker: title
speaker: title
speaker: title

12:30 - 14:15 Lunch

14:15 - 15:15 Session 3:

speaker: title
speaker: title

15:15 - 16:00 Break

16:00 - 17:30 Session 4:

speaker: title
speaker: title
speaker: title

Monday May 10

09:15 - 10:15 Session 5:

speaker: title
speaker: title

10:15 - 11:00 Break

11:00 - 12:30 Session 6:

speaker: title
speaker: title
speaker: title

12:30 - 14:15 Lunch

14:15 - 15:15 Session 7:

speaker: title
speaker: title

15:15 - 16:00 Break

16:00 - 17:30 Session 8:

speaker: title
speaker: title
speaker: title

Tuesday May 11

09:15 - 10:15 Session 9:

speaker: title
speaker: title a lin

10:15 - 11:00 Break

11:00 - 12:00 Session 10:

speaker: title
speaker: title

12:30 - 14:00 Lunch

List of confirmed participants

Parosh Aziz Abdulla	Uppsala
Mohamed Faouzi Atig	Uppsala
Nicolaj Bjorner	Microsoft Research
Ahmed Bouajjani	Paris Diderot
Sylvain Conchon	Paris Sud
Giorgio Delzanno	Genova
Cezara Dragoi	Inria, ENS Paris
Carla Ferreira	Lisboa
Chris Hawblitzel	Microsoft Research
Ranjit Jahala	San Diego
Christoph Kirsch	Salzburg
Igor Konnov	Vienna
Rupak Majumdar	MPI Soft Syst
Ruzica Piskac	Yale
Gustavo Petri	Paris Diderot
Andreas Podelski	Freiburg
Zvonimir Rakamaric	Utah
Marc Shapiro	Inria, Paris UPMC
Thomas Wies	New York
Josef Widder	Vienna