Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 3/2017

09.05.2016

A Decision Procedure for (Co)datatypes in SMT Solvers

verfasst von: Andrew Reynolds, Jasmin Christian Blanchette

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from formalizations developed with Isabelle demonstrates the potential of the procedure.
Vorheriger Artikel Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
Nächster Artikel Abstract Interpretation as Automated Deduction

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
In principle, rank-1 (top-level) polymorphism [8] does not raise any special difficulties. Nesting datatypes inside datatypes, and likewise for codatatypes, can be reduced to the mutual case [19]. So the only genuinely interesting cases missing are mixed nested (co)recursion as well as (co)recursion through a non-(co)datatype (both of which make sense, at least in a higher-order setting [6]).
 
2
It can be convenient to specify the same selector for several constructors associated with the same (co)datatype, as long as the argument types coincide. However, this is disallowed by SMT-LIB, so we do not consider it here.
 
Literatur
1.
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV ’11, LNCS, vol. 6806, pp. 171–177. Springer (2011)
2.
3.
Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisf. Boolean Model. Comput. 3, 21–46 (2007)MathSciNetMATH
4.
Bjørner, N.S.: Integrating decision procedures for temporal verification. Ph.D. thesis, Stanford University (1998)
5.
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)MathSciNetCrossRefMATH
6.
Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 93–110. Springer (2014)
7.
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 131–146. Springer (2010)
8.
Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE-24, LNCS, vol. 7898, pp. 414–420. Springer (2013)
9.
Blanchette, J.C., Popescu, A., Traytel, D.: Witnessing (co)datatypes. In: Vitek, J. (ed.) ESOP 2015, LNCS, vol. 9032, pp. 359–382. Springer (2015)
10.
Carayol, A., Morvan, C.: On rational trees. In: Ésik, Z. (ed.) CSL 2006, LNCS, vol. 4207, pp. 225–239. Springer (2006)
11.
12.
de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE-21, LNCS, vol. 4603, pp. 183–198. Springer (2007)
13.
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008, LNCS, vol. 4963, pp. 337–340. Springer (2008)
14.
Djelloul, K., Dao, T., Frühwirth, T.W.: Theory of finite or infinite trees revisited. Theory Pract. Logic Program. 8(4), 431–489 (2008)MathSciNetCrossRefMATH
15.
Endrullis, J., Grabmayer, C., Klop, J.W., van Oostrom, V.: On equal \(\mu \)-terms. Theor. Comput. Sci. 412(28), 3175–3202 (2011)MathSciNetCrossRefMATH
16.
17.
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(\(T\)): fast decision procedures. In: Alur, R., Peled, D. (eds.) CAV ’04, LNCS, vol. 3114, pp. 175–188. Springer (2004)
18.
Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: CAV ’09, LNCS, vol. 5643, pp. 306–320. Springer (2009)
19.
Gunter, E.L.: Why we can’t have SML-style datatype declarations in HOL. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) TPHOLs ’92, IFIP Transactions, vol. A-20, pp. 561–568. North-Holland/Elsevier (1993)
20.
Hopcroft, J.: An \(n \log n\) algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189–196. Academic Press, London (1971)CrossRef
21.
Jovanović, D., Barrett, C.: Sharing is caring: combination of theories. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011, LNCS, vol. 6989, pp. 195–210. Springer (2011)
22.
Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013, LNCS, vol. 8152, pp. 7–22. Springer (2013)
23.
24.
25.
Leino, K.R.M., Moskal, M.: Co-induction simply—automatic co-inductive proofs in a program verifier. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014, LNCS, vol. 8442, pp. 382–398. Springer (2014)
26.
27.
Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010, LNCS, vol. 6012, pp. 427–447. Springer (2010)
28.
Lochbihler, A.: Making the Java memory model safe. ACM Trans. Program. Lang. Syst. 35(4), 12:1–65 (2014)
29.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefMATH
30.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, LNCS, vol. 2283. Springer (2002)
31.
Pham, T., Whalen, M.W.: RADA: a tool for reasoning about algebraic data types with abstractions. In: Meyer, B., Baresi, L., Mezini, M. (eds.) ESEC/FSE ’13, pp. 611–614. ACM (2013)
32.
Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A., Middeldorp, A. (eds.) CADE-25, LNCS, vol. 9195, pp. 197–213. Springer (2015)
33.
Reynolds, A., Blanchette, J.C., Tinelli, C.: Model finding for recursive functions in SMT. In: Ganesh, V., Jovanović, D. (eds.) SMT 2015 (2015)
34.
Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015, LNCS, vol. 8931, pp. 80–98. Springer (2014)
35.
Reynolds, A., Tinelli, C., Goel, A., Krstić, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE-24, LNCS, vol. 7898, pp. 377–391. Springer (2013)
36.
Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014, pp. 195–202. IEEE (2014)
37.
38.
Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, LNCS, vol. 8562, pp. 367–373. Springer (2014)
39.
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 (2011)
40.
41.
Wand, D.: Polymorphic+typeclass superposition. In: de Moura, L., Konev, B., Schulz, S. (eds.) PAAR 2014 (2014)
42.
Metadaten
Titel
A Decision Procedure for (Co)datatypes in SMT Solvers
verfasst von
Andrew Reynolds
Jasmin Christian Blanchette
Publikationsdatum
09.05.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 3/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9372-6

Weitere Artikel der Ausgabe 3/2017

Journal of Automated Reasoning 3/2017 Zur Ausgabe

OriginalPaper

Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures

EditorialNotes

Preface: Selected Extended Papers of CADE 2015

OriginalPaper

Abstract Interpretation as Automated Deduction

OriginalPaper

Relative Termination via Dependency Pairs