Thesis

Concurrent systems are ubiquitous, ranging from multi-core processors to large-scale distributed systems. Yet, the verification of concurrent systems remains a daunting task, and technological advances such as weak memory architectures greatly compound this problem. Such challenges have renewed interest in symbolic encodings of partial-order semantics of concurrency using propositional logic or decidable fragments of first-order logic. The impetus behind these partial-order encodings is th...