The electrum analyzer: model checking relational first-order temporal specifications

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2018

Autores

Brunel, J (Autor) Outra; Chemouil, D (Autor) Outra; Cunha, A (Autor) Outra; Macedo, N (Autor) Outra

Ata de Conferência Internacional

Título: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018

Páginas: 884-887

33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018

3 September 2018 through 7 September 2018

Indexação

Scopus - 6 Citações

Outras Informações

ID Authenticus: P-00P-KAP

DOI: 10.1145/3238147.3240475

Abstract (EN): 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. Source code: https://github.com/haslab/ElectrumVideo: https://youtu.be/FbjlpvjgMDA. © 2018 Copyright held by the owner/author(s).

Idioma: Inglês

Tipo (Avaliação Docente): Científica