VSL 2014: VIENNA SUMMER OF LOGIC 2014
FRIDA Home Page

FINAL PROGRAM [pdf]

 

In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computer-aided veriļ¬cation of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required.

The topics of interest include but are not limited to:

  • models for distributed algorithms
  • model checking
  • proof assistants & theorem proving
  • parameterized model checking
  • integration of different verification techniques
  • concurrency
  • distributed algorithm theory
  • case studies and benchmarks
  • fault tolerance
  • synthesis
  • automated code generation for distributed systems
  • run-time verification of distributed systems

Rationale

FRIDA is an informal follow-up workshop to a Dagstuhl seminar on formal verification of distributed algorithms (Formal Verification of Distributed Algorithms) held in 2013. In the next years, we continue to organize similar workshops in order to strengthen the collaboration between the concerned communities.

Invited talks

  • Ahmed Bouajjani (Univ. Paris Diderot): On Checking Correctness of Concurrent Data Structures.

[presentation]

  • Joe Halpern (Cornell University): Beyond Nash Equilibrium: Solution Concepts for the 21st Century.

[presentation]

  • Alexander Shvartsman (University of Connecticut): Specifying, Reasoning About, Optimizing, and Implementing Atomic Data Services for Distributed Systems

[presentation]

Regular talks

  • Laure Millet, Maria Gradinariu Potop-Butucaru, Nathalie Sznajder and Sebastien TixeuilOn the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering

[presentation]

  • Noran AzmyHaving SPASS with Pastry and TLA+.
  • Joel RybickiSynthesizing self-stabilizing fault-tolerant algorithms.

[presentation]

[presentation]

  • Sasha RubinAn automata theoretic approach to parameterised verification of robot protocols.
  • Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters and Uwe NestmannMechanical Verification of a Constructive Proof for FLP.

[presentation]

  • Victor Altukhov, Eugene Chemeritskiy, Vladislav Podymov and Vladimir ZakharovModels and techniques for verification of Software Defined Networks.

[presentation]

[presentation]

  • Tobias Gawron-DeutschVerification and Validation Challenges in Smart Grids from the Industrial Perspective.
  • Matthias Függer, Robert Najvirt, Thomas Nowak and Ulrich SchmidTowards binary circuit models that faithfully reflect physical (un)solvability.
  • Ana Sokolova: Concurrent Data Structures: Semantics and (Quantitative) Relaxation.

[presentation]

[presentation]

[presentation]

[presentation]

  • Giorgio Delzanno and Michele TatarekModel Checking Distributed Consensus Algorithms.

[presentation]

Format

This two-day workshop will include invited talks, presentations of position papers, including work-in-progress and published work, and discussion periods. We are planning to collect the abstracts and the presentations for publication on the workshop site. In addition to some invited talks, the program will include short presentations of contributed position papers, a challenge problem session, and ample room for lively discussion and debate on the issues raised.

Important Dates

  • Submission deadline: June 3, 2014
  • Acceptance notification: June 5, 2014
  • Workshop dates: July 23-24, 2014

Submission Instructions

We seek submissions reporting on theory, applications, case studies or open questions at the interface of formal methods and distributed algorithms. Contributions may range from extended abstracts of one or two pages to full papers of twenty pages, in Easychair format, and should be submitted as pdf files. Presentation of papers published elsewhere is acceptable and encouraged. There will be no formal workshop proceedings — therefore, the work will be considered “unpublished”. However, accepted contributions will be made accessible from the Workshop Web page.

Organization

Sponsors

We are grateful to RiSE and Siemens for the sponsor support.

RiSE            Siemens