Dr Ciaran McCreesh - University of Glasgow

Constraint optimisation solvers are computer programs that are used to solve logistics, scheduling, and resource allocation problems where we have resources, constraints on how combinations of those resources may be used, and an objective. These solvers are routinely used to make decisions that affect people’s lives and livelihoods. But why should we trust that these algorithm implementations do not contain bugs? Dr McCreesh’s research involves the design, implementation, and deployment of constraint solvers that ‘show their working’ by producing mathematical proofs alongside their outputs. These proofs can then be audited, allowing independent third parties to guarantee that the solvers have produced the right answers.