The Electrum Analyzer
Channel: Alcino Cunha
Date: 29/05/2018

This video presents the Electrum Analyzer, a free-software tool to validate and perform model checking of Electrum specifications. Electrum is an extension of Alloy that enriches its relational logic with linear temporal logic operators, thus simplifying the specification of dynamic systems. The Analyzer supports both automatic bounded model checking, with an encoding into SAT, and unbounded model checking, with an encoding into SMV. Instance, or counter-example, traces are presented back to the user in a unified visualizer. Features to to speed up model checking are offered, including a decomposed parallel solving strategy and the extraction of symbolic bounds.

Electrum website: https://haslab.github.io/Electrum