Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications Export

@incollection{frias_07_alloy, abstract = {This article contains two main contributions. On the theoretical side, it presents a novel complete proof calculus for Alloy. On the applied side we present Dynamite, a tool that combines the semi-automatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process. As a means to assess the usability of the tool, we present a complex case-study based on Zave\^{a}€™s Alloy model of addressing for interoperating networks.}, author = {Frias, Marcelo and Pombo, Carlos L. and Moscato, Mariano}, citeulike-article-id = {1822676}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-71209-1_46}, citeulike-linkout-1 = {http://dx.doi.org/http://dx.doi.org/10.1007/978-3-540-71209-1_46}, citeulike-linkout-2 = {http://dx.doi.org/10.1007/978-3-540-71209-1_46}, doi = {10.1007/978-3-540-71209-1_46}, journal = {Tools and Algorithms for the Construction and Analysis of Systems}, keywords = {2007, \_folder\_1, alloy, analysis, pvs, verification}, pages = {587--601}, posted-at = {2007-10-26 00:34:54}, priority = {4}, title = {Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications}, url = {http://dx.doi.org/10.1007/978-3-540-71209-1_46}, year = {2007} }

TY - CHAP ID - frias_07_alloy L3 - citeulike-article-id:1822676 N2 - This article contains two main contributions. On the theoretical side, it presents a novel complete proof calculus for Alloy. On the applied side we present Dynamite, a tool that combines the semi-automatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process. As a means to assess the usability of the tool, we present a complex case-study based on Zave’s Alloy model of addressing for interoperating networks. JF - Tools and Algorithms for the Construction and Analysis of Systems EP - 601 TI - Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications SP - 587 KW - 2007 KW - _folder_1 KW - alloy KW - analysis KW - pvs KW - verification AU - Frias, Marcelo AU - Pombo, Carlos AU - Moscato, Mariano PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-71209-1_46 ER -