Neil Menne on The Electrum Analyzer

Full Paper Title: The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications

Description: Alloy is an open source language/analyzer for software modeling; Electrum proposes extensions to Alloy to provide linear temporal logic operators. In so doing, it aims to simplify modeling systems as they change. This paper highlights not just the extensions to the Alloy language but also the Electrum Analyzer which also allows for unbounded model checking.

Bio: Neil is a Senior Backend Engineer I at Bleacher Report. When he's not writing Elixir to keep sports on the internet, he aspires to one day be a competent computer scientist or at least a pragmatic formal methods enthusiast.

Link: https://hal.archives-ouvertes.fr/hal-01846951/document