%0 Book Section %1 frias_07_alloy %A Frias, Marcelo %A Pombo, Carlos L. %A Moscato, Mariano %D 2007 %J Tools and Algorithms for the Construction and Analysis of Systems %K 2007 pvs \_folder\_1 verification \_hardcopy alloy \_pdf analysis %P 587--601 %R http://dx.doi.org/10.1007/978-3-540-71209-1\_46 %T Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications %U http://dx.doi.org/10.1007/978-3-540-71209-1\_46 %X 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.

@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.}, added-at = {2009-03-10T04:37:08.000+0100}, author = {Frias, Marcelo and Pombo, Carlos L. and Moscato, Mariano}, biburl = {https://www.bibsonomy.org/bibtex/2765e4f1341e372636ce7e1417a6850ac/leonardo}, citeulike-article-id = {1822676}, doi = {http://dx.doi.org/10.1007/978-3-540-71209-1\_46}, interhash = {51df9bb9c212db87772f41ca111f1cc6}, intrahash = {765e4f1341e372636ce7e1417a6850ac}, journal = {Tools and Algorithms for the Construction and Analysis of Systems}, keywords = {2007 pvs \_folder\_1 verification \_hardcopy alloy \_pdf analysis}, pages = {587--601}, posted-at = {2007-10-26 00:34:54}, priority = {4}, timestamp = {2009-03-10T04:37:08.000+0100}, 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 }