Skip to main content
SpringerLink
Log in

Exploring Theories with a Model-Finding Assistant

  • Conference paper
  • First Online:
Book cover Automated Deduction - CADE-25 (CADE 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9195))

Included in the following conference series:

Abstract

We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances.

Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models.

Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.

This material is based upon work supported by the National Science Foundation under Grant No. CNS-1116557.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://salmans.github.io/Razor/.

  2. 2.

    The term “geometric” arises from the original study of this class of formulas in the nexus between algebraic geometry and logic [29].

References

  1. Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference On Artificial Intelligence (1995)

    Google Scholar 

  2. McCune, W.: MACE 2.0 Reference Manual and Guide. CoRR (2001)

    Google Scholar 

  3. Claessen, K., Sörensson, N.: New techniques that improve MACE-Style finite model finding. In: CADE Workshop on Model Computation-Principles, Algorithms, Applications (2003)

    Google Scholar 

  4. Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 303–317. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Baumgartner, P., Fuchs, A., De Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Logic 7(1), 58–74 (2009)

    Article  MATH  Google Scholar 

  8. Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Korovin, K., Sticksel, C.: iProver-Eq: an instantiation-based theorem prover with equality. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 196–202. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Bry, F., Torge, S.: A deduction method complete for refutation and finite satisfiability. In: Dix, J., Fariñas del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol. 1489, pp. 122–138. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Baumgartner, P., Suchanek, F.M.: Automated reasoning support for first-order ontologies. In: Alferes, J.J., Bailey, J., May, W., Schwertel, U. (eds.) PPSWR 2006. LNCS, vol. 4187, pp. 18–32. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Jackson, D.: Software Abstractions, 2nd edn. MIT Press, London (2012)

    Google Scholar 

  13. Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: International Conference on Software Engineering (2005)

    Google Scholar 

  14. Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)

    Google Scholar 

  15. Niemelä, I.: A tableau calculus for minimal model reasoning. In: Workshop on Theorem Proving with Analytic Tableaux and Related Methods (1996)

    Google Scholar 

  16. Bry, F., Yahya, A.: Positive unit hyperresolution tableaux and their application to minimal model generation. J. Autom. Reasoning 25(1), 35–82 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  17. Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)

    Google Scholar 

  18. Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Lopes, N., Bjorner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. Technical report, Microsoft Research (2014)

    Google Scholar 

  20. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51, 1–77 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  22. Vickers, S.: Geometric logic as a specification language. In: Imperial College Department of Computing Workshop on Theory and Formal Methods (1995)

    Google Scholar 

  23. Sofronie-Stokkermans, V.: Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems. Electronic Notes on Theoretical Computer Science 230, 161–187 (2009)

    Article  Google Scholar 

  24. Bezem, M., Coquand, T.: Automating coherent logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 246–260. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Maier, D., Mendelzon, A.O., Sagiv, Y.: Testing implications of data dependencies. ACM Trans. Database Syst. 4, 445–469 (1979)

    Article  Google Scholar 

  26. Beeri, C., Vardi, M.Y.: A proof procedure for data dependencies. J. ACM 31(4), 718–741 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  27. Deutsch, A., Tannen, V.: XML queries and constraints, containment and reformulation. ACM Symposium on Theory Computer Science (2005)

    Google Scholar 

  28. Rossman, B.: Existential positive types and preservation under homomorphisms. In: IEEE Logic in Computer Science. IEEE (2005)

    Google Scholar 

  29. Makkai, M., Reyes, G.E.: First Order Categorical Logic. Springer, Heidelberg (1977)

    MATH  Google Scholar 

  30. Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: semantics and query answering. In: Calvanese, D., Lenzerini, M., Motwani, R. (eds.) ICDT 2003. LNCS, vol. 2572, pp. 207–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  31. Deutsch, A., Nash, A., Remmel, J.: The chase revisited. In: ACM Symposium on Principles of Database Systems (2008)

    Google Scholar 

  32. Dougherty, D.J., Guttman, J.D.: Decidability for lightweight Diffie-Hellman protocols. In: IEEE Symposium on Computer Security Foundations, pp. 217–231 (2014)

    Google Scholar 

  33. Saghafi, S., Dougherty, D.J.: Razor: provenance and exploration in model-finding. In: 4th Workshop on Practical Aspects of Automated Reasoning (PAAR) (2014)

    Google Scholar 

  34. Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)

    Article  MATH  Google Scholar 

  35. Nelson, T., Ferguson, A.D., Scheer, M., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. NSDI, April (2014)

    Google Scholar 

Download references

Acknowledgements

We benefitted from discussions with Henning Günther, Joshua Guttman, Daniel Jackson, Shriram Krishnaturthi, Tim Nelson, and John Ramsdell. The name of our tool is homage to Ockham’s Razor (William of Occam 1285–1349): “Pluralitas non est ponenda sine neccesitate”.

Author information

Authors and Affiliations

  1. Worcester Polytechnic Institute, Worcester, MA, USA

    Salman Saghafi, Ryan Danas & Daniel J. Dougherty

Authors
  1. Salman Saghafi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ryan Danas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniel J. Dougherty
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Salman Saghafi .

Editor information

Editors and Affiliations

  1. University of Ottawa, Ottawa, Canada

    Amy P. Felty

  2. University of Innsbruck, Innsbruck, Austria

    Aart Middeldorp

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Saghafi, S., Danas, R., Dougherty, D.J. (2015). Exploring Theories with a Model-Finding Assistant. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21401-6_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-21400-9

  • Online ISBN: 978-3-319-21401-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation