Alloy is a first-order modeling language with a simple

semantics defined in terms of sets and relations. The automatic

analysis of Alloy models is supported by the Alloy Analyzer, a tool

that wisely translates an Alloy model to a propositional formula that

is then analyzed using off-the-shelf SAT-solvers. This analysis is

limited because domain sizes are user-bounded in order to make

analysis feasible. In this talk I will present Dynamite: an extension

of the semi-automatic theorem prover PVS containing a complete

calculus for Alloy, and extensions to PVS that allow one to improve

the proof effort by automatically analyzing new hypotheses with the

aid of the Alloy Analyzer. Dynamite allows to complement the limited

automatic analysis offered by the Alloy Analyzer with semi-automatic

verification through theorem proving.