Kasper Hagens

Ensuring that software behaves as intended is a central challenge in software development. Formal verification provides mathematically rigorous methods for reasoning about programming code. One such method is term rewriting, in which the elementary computational steps defining a program are specified by a set of rewrite rules and the corresponding program behavior is captured by the rewrite relation. The rewrite relation can be seen as a language-independent operational semantics, suitable for defining methods for program analysis, such as termination and complexity analysis. However, a limitation of traditional term rewriting systems is that primitive data structures, such as integers, must be encoded inductively. This does not correspond to the way such data structures are treated in real programming languages. A solution is provided by Logically Constrained Term Rewriting Systems (LCTRSs), where primitive data structures can be treated semantically, thereby providing a more faithful basis for reasoning about program behavior. In this thesis, we use the higher-order extension of LCTRSs, called Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), to study program equivalence. The rewrite relation is used to define a notion of program equivalence, based on the intuition that two programs are equivalent if they exhibit the same input-output behavior. We develop several proof systems to establish program equivalence in practice. All of them are based on well-founded induction over term rewriting systems, which in turn relies on termination, which will therefore play an important role in this thesis. One of the reasons for wanting to have a proof system is to enable computer-guided equivalence proofs. Although program equivalence is undecidable in general (i.e. complete proof automation is not possible), we introduce heuristics to realize a certain degree of automation in simple cases. A substantial part of the thesis is centered around ground confluence. This property is necessary to guarantee the correctness of the method for disproving program equivalence, but it is also important in its own right: in a terminating and ground-confluent system, reduction essentially computes a unique result for every ground term. We develop a method for proving ground confluence of LCSTRSs, and as part of this, we define critical pairs for LCSTRSs.