Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Satisfiability Modulo Bounded Checking

Author : Simon Cruanes

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Satisfiability Modulo Transcendental Functions via Incremental Linearization
next chapter Short Proofs Without New Variables
Footnotes
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
Our framework corresponds to the special case of needed narrowing when the only rewrite rules are those defining pattern matching.
 
4
The example is provided at https://​cedeela.​fr/​~simon/​files/​cade_​17.​tar.​gz along with other benchmarks.
 
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.
 
Literature
1.
2.
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 CrossRef
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)CrossRefMATH
5.
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Not. 46(4), 53–64 (2011)CrossRef
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 CrossRef
7.
8.
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
10.
Duregård, J., Jansson, P., Wang, M.: Feat: functional enumeration of algebraic types. ACM SIGPLAN Not. 47(12), 61–72 (2013)CrossRef
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)
12.
Kaufmann, M., Moore, S.J.: ACL2: an industrial strength version of Nqthm. In: Computer Assurance, COMPASS 1996, pp. 23–34. IEEE (1996)
13.
14.
Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming, pp. 105–123. Citeseer (2007)
15.
16.
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
18.
Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. ACM SIGPLAN Not. 44, 37–48 (2008). ACMCrossRef
19.
Metadata
Title
Satisfiability Modulo Bounded Checking
Author
Simon Cruanes
Copyright Year
2017
Book
Automated Deduction – CADE 26

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

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017

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

Premium Partner

    Image Credits