Declarative Theorem Proving for Operational Semantics

This dissertation is concerned with techniques for formally checking properties of systems that are described by operational semantics. We describe innovations and tools for tackling this problem, and a large case study in the application of these tools.