SPLASH 2020 (series) / ECOOP 2020 (series) / FTfJP 2020 (series) / Formal Techniques for Java-like Programs /
Discourje: Runtime Verification of Communication Protocols in Clojure
I will present Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a formal foundation and is itself implemented in Clojure to offer a seamless specification–implementation experience. Benchmarks show Discourje’s overhead can be less than 5% for real/existing concurrent programs. This is joint work with Ruben Hamers.