Bart Bogaerts

This postdoctoral position at KU Leuven is part of the CertiFOX project, which aims to advance the reliability and correctness of combinatorial optimization software. The project focuses on developing methodologies and tools that guarantee, with 100% certainty, that the correct problem has been solved as specified by the user. Central to this effort is proof logging, where solvers not only provide answers but also machine-verifiable proofs of correctness. The current challenge is to ensure that these proofs relate directly to the human-understandable problem specification, rather than just the low-level translation used by solvers. The successful candidate will conduct research to push the boundaries of proof logging, particularly in making proofs accessible and understandable to humans. This work has significant implications for debugging, auditability, and the rigorous evaluation of algorithmic improvements. The position also includes investigating the connection between formal proofs and human-understandable explanations. The candidate will be expected to mentor PhD and MSc students involved in the project. Applicants must have a PhD in computer science or a closely related field, with strong expertise in combinatorial optimization algorithms such as SAT solving, constraint solving, MaxSAT, SAT modulo theories, Answer Set Programming, and (Mixed) Integer Programming. Proficiency in English is required, and 4–10 years of research experience is expected. The position is fully funded for an initial 12 months, renewable for up to two or three years, and includes a competitive salary or equivalent scholarship, as well as a travel budget. The start date is anticipated to be early 2026, but is negotiable. For further details or inquiries, candidates are encouraged to contact Prof. dr. Bart Bogaerts. Applications should be submitted via the KU Leuven jobsite.