Integrating model checking and theorem proving for relational reasoning

Konstantine Arkoudas, Sarfraz Khurshid, Darko Marinov, Martin Rinard

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRudolf Berghammer, Bernhard Moller, Georg Struth
PublisherSpringer
Pages21-33
Number of pages13
ISBN (Print)354022145X, 9783540221456
DOIs
StatePublished - 2004
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3051
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Integrating model checking and theorem proving for relational reasoning'. Together they form a unique fingerprint.

Cite this