Verification of Recursive Data Types using abstractions
2014-03
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Verification of Recursive Data Types using abstractions
Authors
Published Date
2014-03
Publisher
Type
Thesis or Dissertation
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. In this dissertation, we present 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 into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to address an incompleteness in the previous unrolling algorithm (and associated proof), and then use these notions to address two open problems from previous work: (1) we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and (2) we demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. In addition, we generalize certain kinds of catamorphism functions to support additional parameters. This extension, called parameterized associative-commutative catamorphisms subsumes the associative-commutative class, widens the set of functions that are known to be decidable, and makes several practically important functions (such as forall, exists, and member) over elements of algebraic data types straightforward to express. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-Lib2 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards.
Description
University of Minnesota Ph.D. dissertation. March 2014. Major: Computer Science. Advisors: Michael W. Whalen and Mats P.E. Heimdahl. 1 computer file (PDF); x, 130 pages.
Related to
Replaces
License
Collections
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Suggested citation
Pham, Hung Tuan. (2014). Verification of Recursive Data Types using abstractions. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/163020.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.