Decision Procedures for Equationally Based Reasoning

Hendrix, Joseph D.

Permalink

https://hdl.handle.net/2142/11487 Copy

Description

Title

Decision Procedures for Equationally Based Reasoning

Author(s)

Hendrix, Joseph D.

Issue Date

2008-09

Keyword(s)

computer science

Abstract

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].

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11487

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections