Skip to main content
SpringerLink
Log in

Satisfiability Modulo Bounded Checking

  • Conference paper
  • First Online:
Automated Deduction – CADE 26 (CADE 2017)

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

Included in the following conference series:

Abstract

We describe a new approach to find models for a computational higher-order logic with datatypes. The goal is to find counter-examples for conjectures stated in proof assistants. The technique builds on narrowing [14] but relies on a tight integration with a SAT solver to analyze conflicts precisely, eliminate sets of choices that lead to failures, and sometimes prove unsatisfiability. The architecture is reminiscent of that of an SMT solver. We present the rules of the calculus, an implementation, and some promising experimental results.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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.

    https://cedeela.fr/~simon/files/cade_17_report.pdf.

  2. 2.

    A more flexible definition \(\textsf {depth}(c(t_1,\ldots ,t_n)) = \textsf {cost}(c) + \max _{i=1\ldots n} \textsf {depth}(t_i)\) can also be used to skew the search towards some constructors, as long as \(\text {cost}(c) > 0\) holds for all c.

  3. 3.

    Our framework corresponds to the special case of needed narrowing when the only rewrite rules are those defining pattern matching.

  4. 4.

    The example is provided at https://cedeela.fr/~simon/files/cade_17.tar.gz along with other benchmarks.

  5. 5.

    https://github.com/c-cube/smbc/.

  6. 6.

    https://github.com/Gbury/mSAT.

  7. 7.

    For example, it might be possible to write an efficient interpreter or compiler for use-cases where evaluation is the bottleneck, as long as explanations are tracked accurately and parallel conjunction is accounted for.

References

  1. Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM (JACM) 47, 776–822 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  2. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard Version 2.6 (2016). http://www.SMT-LIB.org

  3. Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 512–526. Springer, Heidelberg (2006). doi:10.1007/11916277_35

    Chapter  Google Scholar 

  4. Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electron. Notes Theor. Comput. Sci. 174(8), 23–37 (2007)

    Article  MATH  Google Scholar 

  5. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Not. 46(4), 53–64 (2011)

    Article  Google Scholar 

  6. Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 333–337. Springer, Cham (2015). doi:10.1007/978-3-319-20615-8_23

    Chapter  Google Scholar 

  7. Claessen, K., Rosén, D.: SAT-based bounded model checking for functional programs (2016) (unpublished). https://github.com/danr/hbmc

  8. The Coq Development Team. The Coq Proof Assistant. http://coq.inria.fr/

  9. Cruanes, S., Blanchette, J.C.: Extending Nunchaku to dependent type theory. In: Blanchette, J.C., Kaliszyk, C. (eds.) Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016. EPTCS, vol. 210, Coimbra, Portugal, pp. 3–12, 1 July 2016

    Google Scholar 

  10. Duregård, J., Jansson, P., Wang, M.: Feat: functional enumeration of algebraic types. ACM SIGPLAN Not. 47(12), 61–72 (2013)

    Article  Google Scholar 

  11. Hanus, M.: A unified computation model for functional and logic programming. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (1997)

    Google Scholar 

  12. Kaufmann, M., Moore, S.J.: ACL2: an industrial strength version of Nqthm. In: Computer Assurance, COMPASS 1996, pp. 23–34. IEEE (1996)

    Google Scholar 

  13. Korf, R.E.: Depth-first iterative-deepening: an optimal admissible tree search. Artif. Intell. 27(1), 97–109 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  14. Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming, pp. 105–123. Citeseer (2007)

    Google Scholar 

  15. Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828. Springer, Heidelberg (1994)

    Book  MATH  Google Scholar 

  16. Reynolds, A., Blanchette, J.C.: A decision procedure for (Co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 197–213. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_13

    Chapter  Google Scholar 

  17. Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 133–151. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_10

    Google Scholar 

  18. Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. ACM SIGPLAN Not. 44, 37–48 (2008). ACM

    Article  Google Scholar 

  19. Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23702-7_23

    Chapter  Google Scholar 

Download references

Acknowledgments

The author would like to thank Jasmin Blanchette, Martin Brain, Raphaël Cauderlier, Koen Claessen, Pascal Fontaine, Andrew Reynolds, and Martin Riener, and the anonymous reviewers, for discussing details of this work and suggesting textual improvements.

Author information

Authors and Affiliations

  1. University of Lorraine, CNRS, Inria, LORIA, 54000, Nancy, France

    Simon Cruanes

Authors
  1. Simon Cruanes
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Cruanes .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Cruanes, S. (2017). Satisfiability Modulo Bounded Checking. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation