On 31 March at 14:00, Mara Miulescu will defend her MSc thesis titled “Computer-Assisted Verification of Partial-Order Reduction Methods”. A summary of her work is given below.

Proving a complex theory correct is difficult; finding a counterexample decades after its publication is even tougher. Recently, correctness issues have been uncovered in several partial-order reduction (POR) theories, older and newer. This has raised the question: are the current methods for proof- checking sufficient, or do we need to take extra precautions? In this thesis, we deem the current approach unreliable, and we propose a new method for researchers to avoid errors in future theories. We demonstrate that an automated theorem prover can be enlisted to find errors, and moreover, that it can automatically find an example that witnesses the errors. To that end, we formalize five partial-order reduction theories with known errors, and reproduce their counterexamples in Alloy. Further, we show that Alloy can prove the absence of counterexamples up to a certain bound. The aim of this thesis is to contribute towards fewer mistakes in future POR methods.