Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/68517
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Brunel, Julien | por |
dc.contributor.author | Chemouil, David | por |
dc.contributor.author | Cunha, Alcino | por |
dc.contributor.author | Macedo, Nuno | por |
dc.date.accessioned | 2020-12-11T17:05:29Z | - |
dc.date.available | 2020-12-11T17:05:29Z | - |
dc.date.issued | 2018-09 | - |
dc.identifier.citation | Brunel, J., Chemouil, D., Cunha, A., & Macedo, N. (2018, September). The electrum analyzer: model checking relational first-order temporal specifications. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (pp. 884-887) | por |
dc.identifier.isbn | 9781450359375 | por |
dc.identifier.issn | 1527-1366 | por |
dc.identifier.uri | https://hdl.handle.net/1822/68517 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | European Regional Development Fund (ERDF) through the Operational Programme for Competitiveness and Internationalisation (COMPETE2020) and by National Funds through the Portuguese funding agency, Fundação para a Ciência e a Tecnologia (FCT) within project POCI-01-0145-FEDER-016826, and the French Research Agency project FORMEDICIS ANR-16-CE25-0007 | por |
dc.language.iso | eng | por |
dc.publisher | Association for Computing Machinery (ACM) | por |
dc.rights | openAccess | por |
dc.subject | Formal specification language | por |
dc.subject | Model checking | por |
dc.subject | Model validation | por |
dc.title | The electrum analyzer: Model checking relational first-order temporal specifications | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://dl.acm.org/doi/10.1145/3238147.3240475 | por |
oaire.citationStartPage | 884 | por |
oaire.citationEndPage | 887 | por |
oaire.citationConferencePlace | Montpellier, France | por |
dc.date.updated | 2020-12-11T15:20:29Z | - |
dc.identifier.doi | 10.1145/3238147.3240475 | por |
dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
dc.subject.wos | Science & Technology | por |
sdum.export.identifier | 7588 | - |
sdum.journal | Proceedings IEEE International Automated Software Engineering Conference | por |
sdum.conferencePublication | ASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
ase18tool.pdf | 578,54 kB | Adobe PDF | Ver/Abrir |