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.
Users
Please
log in to take part in the discussion (add own reviews or comments).