Joe Hendrix
Personal email
j[my last name]@whoisjoe.info
Welcome
I develop software for helping people find bugs in their own systems. I recently finished my Ph.D. in computer science at The University of Illinois at Urbana-Champaign, and will be joining Microsoft this fall.
Originally from Austin, Texas, I was in Plan 2 and studied computer science at The University of Texas. I developed software for geotechnical engineering, enterprise systems, and the healthcare industry. I've held summer research positions at NASA Ames in Mountain View, AIST in Japan, and Microsoft Research in Redmond. I tend to not talk very much when meeting new people, but usually warm up quite quickly — especially over a good beer.
Software
-
Overview
The Maude Sufficient Completeness Checker is a tool designed to check that each operation in a terminating and Church-Rosser Maude specification is defined on all valid inputs for confluent and terminating Maude specifications. The tool currently comes in two different versions, each with different features:
- A narrowing-based tool integrated with the Maude Inductive Theorem Prover for checking the sufficient completeness of membership equational specifications with only commutativity axioms, and
- A newer tree automata-based tool for checking the sufficient completeness of order-sorted, linear specifications with rewriting modulo associativity, commutativity, and identity.
- Ceta: A Library for Equational Tree AutomataOverview
Ceta is a library for reasoning about combinations of equational tree languages. It supports emptiness testing of tree languages definable by a boolean combination of regular tree automaton over an equational theory containing operators that have any combination of associativity, commutativity, and identity axioms. Ceta is based on propositional tree automata, and offers algorithms and data structures for representing tree automata, combining tree automata using boolean operations, and testing emptiness.
Publications
-
Combining Equational Tree Automata Over AC and ACI TheoriesAccepted at RTA 2008. See technical report below for an extended version.Abstract
In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories imply similar decidability results in the combined theory; (2) checking emptiness of a language obtained from the Boolean combination of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a non-modular property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule f(x,x) -> x rather than an equation f(x,x) = x, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If E contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular E-tree languages?
-
Diffie-Hellman Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
-
The Maude Formal Tool EnvironmentAbstract
This paper describes the main features of several tools concerned with the analysis of either Maude specifications, or of extensions of such specifications: the ITP, MTT, CRC, ChC, and SCC tools, and Real-Time Maude for real-time systems. These tools, together with Maude itself and its searching and model-checking capabilities, constitute Maude's formal environment.
-
On the Completeness of Context-Sensitive Order-sorted SpecificationsIn Proc. of RTA 2007, LNCS 4533, Springer-Verlag, 229–245 (preprint Tech. Report UIUCDCS-R-2007-2812).Abstract
We propose three different notions of completeness for order-sorted equational specifications supporting context-sensitive rewriting modulo axioms relative to a replacement map μ. Our three notions are: (1) a definition of μ-canonical completeness under which μ-canonical forms coincide with canonical forms; (2) a definition of semantic completeness that guarantees that the μ-operational semantics and standard initial algebra semantics are isomorphic; and (3) an appropriate definition of μ-sufficient completeness with respect to a set of constructor symbols. Based on these notions, we use equational tree automata techniques to obtain decision procedures for checking these three kinds of completeness for equational specifications satisfying appropriate requirements such as weak normalization, ground confluence and sort-decreasingness, and left-linearity. The decision procedures are implemented as an extension of the Maude sufficient completeness checker.
-
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo AxiomsAbstract
We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.
-
Propositional Tree AutomataIn Proc. of RTA 2006, LNCS 4098, Springer-Verlag, 50–65, and also available as Tech. Report UIUCDCS-R-2006-2695.Abstract
We introduce a new tree automata framework, called Propositional Tree Automata, capturing the class of tree languages that are closed under an equational theory and Boolean operations. This framework originates in work on developing a sufficient completeness checker for specifications with rewriting modulo an equational theory. Propositional tree automata recognize regular equational tree languages. However, unlike regular equational tree automata, the class of propositional tree automata is closed under Boolean operations. This extra expressiveness does not affect the decidability of the membership problem. This paper also analyzes in detail the emptiness problem for propositional tree automata with associative theories. Though undecidable in general, we present a semi-algorithm for checking emptiness based on machine learning that we have found useful in practice.
-
A Sufficient Completeness Reasoning Tool for Partial SpecificationsAbstract
We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a backend to try to automatically discharge those proof obligations.
-
Matrices in ACL2In Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003). (Postscript) (Source Code)Abstract
This paper describes a formalization matrices in ACL2. The work defines basic linear algebra operations on matrices, and proves many basic theorems to simplify reasoning about them.
Technical Reports
-
Combining Equational Tree Automata Over AC and ACI TheoriesAvailable here. 30 pages. Slightly older version available as Tech. Report UIUCDCS-R-2008-2940.Abstract
In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories imply similar decidability results in the combined theory; (2) checking emptiness of a language obtained from the Boolean combination of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a non-modular property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule f(x,x) -> x rather than an equation f(x,x) = x, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If E contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular E-tree languages?
-
Sufficient Completeness Checking with Propositional Tree AutomataAvailable as Tech. Report UIUCDCS-R-2005-2635.Abstract
Sufficient completeness means that enough equations have been specified, so that the functions of an equational specification are fully defined on all relevant data. This is important for both debugging and formal reasoning. In this work we extend sufficient completeness methods to handle expressive specifications involving: (i) partiality; (ii) conditional equations; and (iii) deduction modulo axioms. Specifically, we give useful characterizations of the sufficient completeness property for membership equational logic (MEL) specifications having features (i)--(iii). We also propose a kind of equational tree automata, called Propositional Tree Automata (PTA) and identify a class of MEL specifications (called PTA-checkable) whose sufficient completeness problem is equivalent to the emptiness problem of their associated PTA. When the reasoning modulo involves only symbols that are either associative and commutative (AC) or free, we further show that the emptiness of AC-PTA is decidable, and therefore that the sufficient completeness of AC-PTA-checkable specifications is decidable. The methods presented here can serve as a basis for building a next-generation sufficient completeness tool for MEL specifications having features (i)--(iii). These features are widely used in practice, and are supported by languages such as Maude and other advanced specification and equational programming languages.