Reasoning about programs with Mathematical Execution
Zhoulai Fu, University of California, Davis
Room: 3A08
Time: Thu 27 Apr 2017 at 13:00-14:00
Host: Claus Brabrand

Abstract:

I will present Mathematical Execution (ME), an unconventional,
interdisciplinary PL paradigm for ensuring 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 is a unified approach.
It 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. 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.