Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

01.12.2016 | Ausgabe 4/2016

Journal of Automated Reasoning 4/2016

Reasoning About Algebraic Data Types with Abstractions

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 4/2016
Autoren:
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen

Abstract

Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain. We show that the procedure is sound and complete for a class of catamorphisms that satisfy a generalized sufficient surjectivity condition. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We use the generalized sufficient surjectivity condition to address an incompleteness in the previous unrolling algorithm (and associated proof). We then propose the categories of monotonic and associative catamorphisms, which we argue provide a more intuitive inclusion test than the generalized sufficient surjectivity condition. We use these notions to address two open problems from previous work: (1) we provide a bound, with respect to formula size, on the number of unrollings necessary for completeness, showing that it is linear for monotonic catamorphisms and exponentially small for associative catamorphisms, and (2) we demonstrate that associative catamorphisms can be combined within a formula while preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-LIB 2.0 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Premium Partner

    Bildnachweise