Joe Hendrix
What Did I Forget?
Using Equational Tree Automata to Identify Incomplete Specifications

Abstract: Sometimes the mistake lies not in what is stated, but what is left unstated. A specification is "sufficiently complete" when all of the operations are defined on the relevant data. A function that operates on lists without considering the empty list is not sufficiently complete.

In this presentation, I will describe the sufficient completeness problem for equational specifications, and show how it can be checked by casting the problem as a tree language problem. Techniques that I have developed for a theoretical framework called equational tree automata can then be used to automatically check sufficient completeness of many specifications.

Equational tree automata is a theoretical framework that can be used for representing and reasoning about potentially infinite sets of trees. The equations are used to identify trees which are syntactically different, but represent the same semantic value. This is useful in verifying properties of data structures such as lists, queues, and sets where syntactically different structures may be used to represent the same underlying data.

Sufficient completeness is just one application of equational tree automata. Other applications include protocol verification, analyzing the semantics of lazy evaluation, and XML schema. I will discuss these applications, recent theoretical developments in the area, and my C++ library CETA which allows developers to solve their own equational tree automata problems. This talk will not assume previous familiarity with equational specification or tree automata.


Bio: Joe Hendrix is a Ph.D. candidate at the University of Illinois at Urbana-Champaign. His research focuses on developing algorithms and tools for software verification. He has had internships and visiting positions at Microsoft Research, Advanced Institute of Science and Technology in Amagasaki, Japan, and NASA Ames Research Center. Prior to graduate school, he was a software developer in Austin, Texas.

Appointments: dcm@cs.cmu.edu


Maintainer Home > Seminar ]
`Last modified: Wed 27 Jun 11:09:10 EDT 2008