TY - CHAP

T1 - Integrating model checking and theorem proving for relational reasoning

AU - Arkoudas, Konstantine

AU - Khurshid, Sarfraz

AU - Marinov, Darko

AU - Rinard, Martin

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35048836124&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048836124&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24771-5_3

DO - 10.1007/978-3-540-24771-5_3

M3 - Chapter

AN - SCOPUS:35048836124

SN - 354022145X

SN - 9783540221456

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 21

EP - 33

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Berghammer, Rudolf

A2 - Moller, Bernhard

A2 - Struth, Georg

PB - Springer

ER -