COPLAS talk by Zhoulai Fu

Topic: Program Reasoning with Mathematical Execution

Speaker: Zhoulai Fu, IT University of Copenhagen


I will present a new, general method for reasoning about program correctness. The idea is to reduce the problem of verifying/testing a program into that of minimizing a derived representing function, which avoids static or symbolic reasoning about the program semantics. ME has proved to be highly efficient on programs that are heavy on numerical calculations, including floating-point arithmetic, non-linear variable relationship, and external function calls. It is a unified approach. For example, on satisfiability solving, ME performs hundreds of times faster than MathSat and Microsoft’s Z3; on coverage-based testing, ME outperformed Google’s security-oriented fuzz tester AFL by 18% of branches on Sun’s math library.


Zhoulai Fu is Assistant Professor in the Computer Science Department at the IT University of Copenhagen since 2017, where he works in the Software Quality Research Group. Earlier, he graduated from Ecole Polytechnique, France, obtaining his doctoral degree at INRIA, and then he did a postdoc at University of California at Davis. His primary research interest lies in approaching software engineering problems from a mathematical or programming language perspective.  A particular category of such problems is numerical code analysis, on which he has developed satisfiability solving and automated testing tools that outperform the state-of-the-art significantly.  At the IT University, Zhoulai Fu works in an EU Horizon 2020 research project, where his role is to develop effective and scalable program analysis/testing approaches for assurance software quality of the Robotic Operation System (ROS).

All are welcome. No registration required. Apres-talk discussion and TGIF at 3 p.m.

Contact: Fritz Henglein, +45 30589576