一句话：提出 Electrum Analyzer，为 Alloy 关系逻辑扩展 LTL，并支持有界 SAT 与无界 SMV 模型检测及可视化加速。
本文介绍 Electrum Analyzer，一个用于验证和模型检测 Electrum 规约的自由软件工具。Electrum 在 Alloy 的关系逻辑上加入 LTL 算子，以便更简洁地描述动态系统。该分析器同时支持有界模型检测（编码为 SAT）和无界模型检测（编码为 SMV），并将实例或反例轨迹在统一的可视化器中返回给用户。工具还提供加速模型检测的功能，包括分解式并行求解策略和符号边界提取。
This paper 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 LTL 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 speed up model checking are offered, including a decomposed parallel solving strategy and the extraction of symbolic bounds.
@inproceedings{paperbot4793,
title = {The electrum analyzer: model checking relational first-order temporal specifications},
author = {Julien Brunel and David Chemouil and Alcino Cunha and Nuno Macedo},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240475}
}