Please note: This PhD seminar will take place in DC 2564 and online.
Xintong Zhou, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Chengnian Sun
Mixed-integer programming (MIP) is a fundamental class of mathematical optimization problems with broad applications in various domains such as finance, engineering, and management science. MIP solvers, software systems that automatically solve MIP problems, serve as the computational backbone for these applications. Given their widespread use, ensuring the correctness of MIP solvers is crucial, as incorrect results, such as falsely determining feasibility or returning incorrect solutions, can lead to serious real-world consequences. Despite its importance, validating the correctness of MIP solvers remains largely unexplored in both theory and practice.
This paper presents the first systematic effort to address this problem. We propose feasibility-driven instance generation, a simple yet effective technique to generate random MIP instances for testing solver correctness. The core idea is to systematically synthesize MIP instances that are provably feasible or infeasible by construction. These instances are then fed to MIP solvers to detect potential bugs. We realize this methodology in Flip. To date, Flip has uncovered 67 confirmed bugs in five widely used MIP solvers, spanning both open-source and commercial systems. Among these, 54 have been promptly fixed by the developers. Our efforts and findings have been well acknowledged by the MIP solver community.
To attend this PhD seminar in person, please go to DC 2564. You can also attend virtually on Zoom.