Integrating Model Checking and Theorem Proving for Relational Reasoning

  • Konstantine Arkoudas
  • Sarfraz Khurshid
  • Darko Marinov
  • Martin Rinard
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


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.


Model Check Theorem Prove Transitive Closure Relational Reasoning Proof Obligation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    TPTP problem library for automated theorem proving,
  2. 2.
    Arkoudas, K.: Type-ω DPLs. MIT AI Memo 2001-27 (2001)Google Scholar
  3. 3.
    Frias, M.F.: Fork Algebras in Algebra, Logic and Computer Science. World Scientific Publishing Co., Singapore (2002)zbMATHCrossRefGoogle Scholar
  4. 4.
    Frias, M.F., Pombo, C.G.L., Baum, G.A., Aguirre, N.M., Maibaum, T.: Taking alloy to the movies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)Google Scholar
  5. 5.
    Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  6. 6.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  7. 7.
    Jackson, D.: Micromodels of software: Modelling and analysis with Alloy (2001),
  8. 8.
    Jackson, D., Schechter, I., Shlyakhter, I.: ALCOA: The Alloy constraint analyzer. In: Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland (June 2000)Google Scholar
  9. 9.
    Jackson, D., Sullivan, K.: COM revisited: Tool-assisted modeling of an architectural framework. In: Proc. 8th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), San Diego, CA (2000)Google Scholar
  10. 10.
    Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: Proc. 15th IEEE International Conference on Automated Software Engineering (ASE), Grenoble, France (September 2000)Google Scholar
  11. 11.
    Khurshid, S., Marinov, D., Jackson, D.: An analyzable annotation language. In: Proc. ACM SIGPLAN 2002 Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Seattle, WA (November 2002)Google Scholar
  12. 12.
    Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA (November 2001)Google Scholar
  13. 13.
    McCune, W.: Mace: Models and counter-examples (2001),
  14. 14.
    Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)Google Scholar
  15. 15.
    Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)zbMATHGoogle Scholar
  16. 16.
    Pombo, C.L., Owre, S., Shankar, N.: A semantic embedding of the ag dynamic logic in PVS. Technical Report SRI-CSL-02-04, SRI International, Menlo Park, CA (May 2003)Google Scholar
  17. 17.
    Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3) (2002)Google Scholar
  18. 18.
    Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking with automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)Google Scholar
  19. 19.
    Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 1. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Vaziri, M., Jackson, D.: Checking properties of heap-manipulating procedures with a constraint solver. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 505–520. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    Wos, L., Overbeek, R., Lusk, E., Boyle, J.: Automated Reasoning, Introduction and Applications. McGraw-Hill, Inc., New York (1992)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Konstantine Arkoudas
    • 1
  • Sarfraz Khurshid
    • 1
  • Darko Marinov
    • 1
  • Martin Rinard
    • 1
  1. 1.MIT Laboratory for Computer ScienceCambridgeUSA

Personalised recommendations