Conference
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
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. …
Authors
Frias. MF; Pombo CGL; Moscato MM
Series
Lecture Notes in Computer Science
Volume
4424
Pagination
pp. 587-601
Publisher
Springer Nature
Publication Date
2007
DOI
10.1007/978-3-540-71209-1_46
Conference proceedings
Lecture Notes in Computer Science
ISSN
0302-9743