Prototype Verification System (PVS)

PVS is a system consisting of a specification language and a theorem prover. We are using it to encode an equivalence notion for object models, and a type system and semantics for Alloy. They will be used to prove in PVS that our transformations are sound. Moreover, it will be used to prove some properties of our equivalence notion.

• PVS's Home Page

• PVS Language

• PVS Prover

Back