Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/26533
Título: | Giving ALLOY a family |
Autor(es): | Neves, Renato Madeira, Alexandre Martins, Manuel A. Barbosa, L. S. |
Palavras-chave: | Theorem provers Alloy |
Data: | Set-2013 |
Editora: | IEEE |
Resumo(s): | Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. ALLOY is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to other tools in order to meet such challenges. This paper’s proposal, however, is not establishing a link from ALLOY to another single tool, but rather to “plunge” it into the HETS network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. Semantical foundations for this integration are discussed in detail. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/26533 |
ISBN: | 9781479910502 |
DOI: | 10.1109/IRI.2013.6642513 |
Versão da editora: | http://dx.doi.org/10.1109/IRI.2013.6642513 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
NBMM13-iri.pdf | Main article (preprint) | 391,11 kB | Adobe PDF | Ver/Abrir |