Content area
Every person who writes software must contend with finding and fixing coding errors. Detecting software defects is difficult and time consuming, and the cost of missed bugs can be high. While best practices for reducing errors in practical software development tend to focus on techniques such as code review and testing, formal verification is the the most robust method for guaranteeing a piece of software will behave in accordance with its specification. Formal verification for practical software engineering is becoming increasingly available, with most modern programming languages targeted by at least one formal verification tool. Verification-aware languages like Dafny offer the ability to write code directly tailored to automated formal verification, and are backed by significant engineering resources. However, many industrial-strength verification tools and techniques are limited to reasoning about single program executions, while several important relational properties can only be stated in terms of multiple program runs. Furthermore, many of these tools are designed to verify safety properties, properties that require a program to "never go wrong", while many properties of practical importance have liveness components, which require the possibility that a program "may go right". While many formal verification techniques exist which can handle relational and liveness properties, they tend to either require bespoke tooling which can not leverage the engineering resources behind major single-program verifiers, or do not offer automated approaches at all.
Advancing the state of pragmatic formal verification requires tools and techniques which can handle a variety of relational program properties, and which can leverage the substantial engineering effort behind existing verifiers. This dissertation investigates specification and automatic verification of important relational properties, including properties with liveness components. It additionally presents a novel technique for automating discovery of program alignments, allowing existing single-program verifiers to be used in automated relational verification.