%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 }