Please use this identifier to cite or link to this item:
|Title:||Giving Alloy a family|
|Authors:||Renato Jorge Neves|
Alexandre Castro Madeira
Luís Soares Barbosa
|Abstract:||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. © 2013 IEEE.|
|Appears in Collections:||HASLab - Articles in International Conferences|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.