Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/34744
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Neves, Renato | por |
dc.contributor.author | Madeira, Alexandre | por |
dc.contributor.author | Martins, Manuel A. | por |
dc.contributor.author | Barbosa, L. S. | por |
dc.date.accessioned | 2015-04-07T15:30:24Z | - |
dc.date.available | 2015-04-07T15:30:24Z | - |
dc.date.issued | 2014 | - |
dc.identifier.isbn | 978-3-319-04716-4 | - |
dc.identifier.issn | 2194-5357 | - |
dc.identifier.uri | https://hdl.handle.net/1822/34744 | - |
dc.description | Publicado em "Integration of reusable systems". ISBN 978-3-319-04716-4 | por |
dc.description.abstract | Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need for more sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic. | por |
dc.description.sponsorship | (undefined) | por |
dc.language.iso | eng | por |
dc.publisher | Springer International Publishing AG | por |
dc.rights | openAccess | por |
dc.subject | Model finding | por |
dc.subject | Theorem proving | por |
dc.subject | Second–order logic | por |
dc.title | An institution for Alloy and its translation to second-order logic | por |
dc.type | bookPart | por |
dc.peerreviewed | yes | por |
dc.comments | 1507 | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 45 | por |
oaire.citationEndPage | 75 | por |
oaire.citationTitle | Advances in intelligent systems and computing | por |
oaire.citationVolume | 263 | por |
dc.publisher.uri | Advances in Intelligent Systems and Computing, Thouraya Bouabana Tebibel and Stuart H. Rubin (eds) | por |
dc.identifier.doi | 10.1007/978-3-319-04717-1_3 | por |
sdum.journal | Advances in intelligent systems and computing | por |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |