Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 09:00 - 09:30 at Erlang - Session 1 Chair(s): Viktória Fördős

Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure.
Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find.
But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly.
Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations.
Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.

In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course.
We argue that broadcast algorithms provide a sweet spot in design and verification complexity.
To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification.
TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things.
Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems.
Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.

Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

07:50 - 09:30: Session 1Erlang at Erlang
Chair(s): Viktória FördősCisco Systems
07:50 - 08:00
Day opening
Opening
Erlang
Annette BieniusaTechnische Universität Kaiserslautern, Viktória FördősCisco Systems
08:00 - 08:30
Short-paper
Transformations towards Clean Functional Code
Erlang
Boldizsár PoórEötvös Loránd University, Melinda TothEötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd., István BozóEötvös Loránd University
DOI
08:30 - 09:00
Talk
Supporting Secure Coding with RefactorErl
Erlang
Brigitta BaranyaiELTE Eötvös Loránd University, István BozóEötvös Loránd University, Melinda TothEötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd.
09:00 - 09:30
Full-paper
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Erlang
Peter ZellerTU Kaiserslautern, Annette BieniusaTechnische Universität Kaiserslautern, Carla FerreiraUniversidade Nova Lisboa
DOI