|
My main research goal is to find ways to use the computation power
available today to make improvements in the development process of
the next generation of systems.
My main expertise and interests lay in the areas term of rewrite systems,
automated theorem proving, and automata theory.
Due to the complexity of today's systems, automating software
verification is quite difficult, but the benefits are enormous. I
feel that making significant progress in this area requires both strong
theoretical skills and a practical focus, and work hard to better myself
in both aspects.
Currently, I am a graduate student in computer science at The University of Illinois at Urbana-Champaign.
I am a member of the Formal Methods and Declarative Languages Laboratory and a student of
José Meseguer.
I've held summer research positions
at NASA Ames in Mountain View,
AIST in Japan,
and Microsoft Research in Redmond.
In what seems like a previous life, I developed software for geotechnical engineering, enterprise systems, and
the healthcare industry.
I am originally from Austin, Texas. I was in Plan 2
and studied computer science at The University of Texas.
I became interested in formal methods while doing an undergraduate thesis under the
direction of J Moore.
I enjoy programming in Maude, C++, and
ACL2. I enjoy reading
difficult books.
I tend to not talk very much when meeting new people, but usually warm up quite quickly.
I've reviewed papers for
IJCAR 2006, LPAR 2005, LPAR 2007, RTA 2005–07, and I helped prepare
Joseph Goguen's Festschrift.
-
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 Automata
Overview
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.
-
Combining Equational Tree Automata Over AC and ACI Theories
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 Environment
Abstract
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 Specifications
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 Axioms
Abstract
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 Automata
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 Specifications
Abstract
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 ACL2
Joe Hendrix
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.
-
Combining Equational Tree Automata Over AC and ACI Theories
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 Automata
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.
|
