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.
%0 Book Section
%1 arkoudas_04_integrating
%A Arkoudas, Konstantine
%A Khurshid, Sarfraz
%A Marinov, Darko
%A Rinard, Martin
%D 2004
%J Relational and Kleene-Algebraic Methods in Computer Science
%K _hardcopy 2004 alloy _no_doi theorem_prover model_checking
%P 21--33
%T Integrating Model Checking and Theorem Proving for Relational Reasoning
%U http://www.springerlink.com/content/3y9ckdklkkeumxk0
%X 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.
@incollection{arkoudas_04_integrating,
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.},
added-at = {2009-02-11T21:04:48.000+0100},
author = {Arkoudas, Konstantine and Khurshid, Sarfraz and Marinov, Darko and Rinard, Martin},
biburl = {https://www.bibsonomy.org/bibtex/2f26cc93a624cd19b246fe9d9610ae91d/leonardo},
citeulike-article-id = {1569389},
interhash = {b68e1b68cf8e7dcd9ac0f596b634955e},
intrahash = {f26cc93a624cd19b246fe9d9610ae91d},
journal = {Relational and Kleene-Algebraic Methods in Computer Science},
keywords = {_hardcopy 2004 alloy _no_doi theorem_prover model_checking},
pages = {21--33},
posted-at = {2007-08-16 14:51:05},
priority = {4},
timestamp = {2009-02-11T21:04:48.000+0100},
title = {Integrating Model Checking and Theorem Proving for Relational Reasoning},
url = {http://www.springerlink.com/content/3y9ckdklkkeumxk0},
year = 2004
}