Decision Procedures for Equationally Based Reasoning

This work develops new automated reasoning techniques for verifying the correctness of equationally specified programs. These techniques are not just theoretical, but have been implemented, and applied to actual program verification projects. Although the work spans several different areas, a major theme of this work is to develop better techniques at the boundary between decidable and undecidable problems. That is, this work seeks out not just positive decidability results, but ways to extend the underlying techniques to be effective on problems outside of decidable subclasses. For program verification to succeed, we feel that two important directions must be pursued: (1) considering more expressive logics to allow designers to more easily specify systems, and (2) develop decision procedures that can reason efficiently about these more sophsticated logics. This work pursues both directions, and the main topics addressed include: new decidability and undecidability results for equational tree automata (Chapter 3), order-sorted unification (Chapter 4), sufficient completeness for specifications with partiality and rewriting modulo axioms (Chapter 5), completeness problems for contextsensitive specifications (Chapter 6), coverset induction in membership equational logic (Chapter 7), and a case study for verifying properties of powerlists with the Maude ITP (Chapter 8). Each of these theoretical topics have lead to the development of new libraries and tools. Two of the tools have already been used in external projects including our tree automata library's integration into the ACTAS protocol verification tool [126], and the order-sorted unification procedures use in the Maude-NRL protocol analyzer [49]