%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 model\_checking 2004 \_hardcopy alloy \_no\_doi \_pdf theorem\_prover %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 tool that integrates model checking and theorem proving for relational reasoning. Prioni takes as input formulas written in Alloy, a declarative language based on relations. Prioni uses the Alloy Analyzer to check the validity of Alloy formulas for a given scope that bounds the universe of discourse. The Alloy Analyzer can refute a formula if a counterexample exists within the given scope, but cannot prove that the formula holds for all scopes. For proofs, Prioni uses Athena, 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-03-10T04:38:22.000+0100}, author = {Arkoudas, Konstantine and Khurshid, Sarfraz and Marinov, Darko and Rinard, Martin}, biburl = {https://www.bibsonomy.org/bibtex/2fc8d433e2fff46a73020d5ff233a845e/leonardo}, citeulike-article-id = {1569389}, interhash = {0729ae019a36e4ff9e1e104421672cc0}, intrahash = {fc8d433e2fff46a73020d5ff233a845e}, journal = {Relational and Kleene-Algebraic Methods in Computer Science}, keywords = {model\_checking 2004 \_hardcopy alloy \_no\_doi \_pdf theorem\_prover}, pages = {21--33}, posted-at = {2007-08-16 14:51:05}, priority = {4}, timestamp = {2009-03-10T04:38:22.000+0100}, title = {Integrating Model Checking and Theorem Proving for Relational Reasoning}, url = {http://www.springerlink.com/content/3y9ckdklkkeumxk0}, year = 2004 }