2 talks, one about Lithium and the other about Stainless

In this session we are going to have two talks, here are the description:

Stainless by Romain Ruetschi

Given the fundamental difficulty of writing bug-free code, academia and industry have come up over the years with various mitigation techniques, such as writing unit- or property-based tests, designing more expressive type systems, performing code reviews. Formal software verification is another important technique which allows developers to statically verify that their software systems will never crash nor diverge, and will in addition satisfy given functional correctness properties.

In this talk, I will present Stainless, a formal verification tool for Scala which can help develop highly reliable applications, with errors caught early during the development process. Thanks to its use of formal methods, Stainless can establish safety and termination properties using symbolic reasoning, covering infinitely many inputs in a single run of verification.

I will also demonstrate the tooling we have developed around Stainless which lets users easily integrate Stainless in their Scala projects via sbt.

Lithium by Dennis van der Bij

When using Akka-cluster, when some nodes become unreachable, no one can join or even leave the cluster anymore. To bring back the cluster to a fully working state, the unreachable nodes must be downed. However, because there is no way of knowing if a node has crashed or is victim of a network partition, if done incorrectly the downing could lead to data corruption, a split-brain, and a headache fixing it.

In order to automatically and correctly recover from unreachable nodes, Lightbend provides a resolver through it’s subscription. For individuals and companies that cannot afford the subscription, some open-source solutions exist but do not come near it in terms of features and correctness. To fix that gap, I developped an open-source split-brain resolver called Lithium as part of my EPFL master project.

In this talk I will introduce Lithium, explain how it works helps with recovering the cluster from unreachable nodes, its internals, and everything to know to set it up.

Bio:

Romain Ruetschi:
Romain Ruetschi earned a MSc degree in Computer Science from EPFL in February 2018, and has since been working at the Laboratory for Automated Reasoning and Analysis (LARA) at EPFL, under the supervision of Prof. Viktor Kunčak. He is nowadays one of the main contributor to the Stainless verification system.

Dennis van der Bij:
I learned about Scala, as every EPFL computer science student, through the Coursera course. Three years ago I discovered pure FP by reading “FP in Scala” by Chiusano and Bjarnason. I have been developping using Scala since then. I’ve been developping Lithium, an open-source split-brain resolver for Akka, while being an intern at SwissBorg. I now work there as a software engineer working on the next evolution in crypto wealth-management.