Incollection,
Integrating Model Checking and Theorem Proving for Relational Reasoning
(2004)
Abstract
We present Prioni, a^A tool that integrates model checking and theorem proving for relational reasoning. Prioni takes as input formulas written in Alloy, a^A declarative language based on relations. Prioni uses the Alloy Analyzer to check the validity of Alloy formulas for a^A given scope that bounds the universe of discourse. The Alloy Analyzer can refute a^A formula if a^A counterexample exists within the given scope, but cannot prove that the formula holds for all scopes. For proofs, Prioni uses Athena, a^A denotational proof language. Prioni translates Alloy formulas into Athena proof obligations and uses the Athena tool for proof discovery and checking.
