When all abstraction is lost

Scala Days Copenhagen 2017

Did you ever implement an asynchronous/distributed algorithm or data structure and wondered whether your implementation is correct? Did you ever try to solve this problem by testing thoroughly and a little bit of reasoning with the result being “the system will probably work correctly”? If you answered to any of these question with yes then this talk is definitely for you.

In this Talk we will look at a novel approach to easily prove the correctness of concurrent/distributed systems with the help of an extension for ScalaTest. The extension offers a DSL for describing behaviors of these systems and employs explicit state model checking for the purpose of proofing those behaviors. Since, model checking isn’t widely used in the Scala world we will (briefly) discuss this concept before looking at the DSL and extension itself. In the demo we will see that the extension can be used for proofing the correctness of a real-world system written in Scala.

Monads will not be mentioned during this Talk. However, the audience may be exposed to a non-painful amount of temporal logic.

Recording of the talk: https://www.youtube.com/watch?v=2E8d8hjph0U