'High-Assurance Scientific Computing', Zhoulai Fu, IT University of Copenhagen

Dates: 
Wednesday, July 7, 2021 - 11:00am to 1:10pm
Location: 
Zoom - contact events@cs.stonybrook.edu for Zoom info.
Event Description: 

Talk abstract: 

Floating-point software is at the heart of today's scientific computing, engineering, and cyber-physical systems. Such software is pervasive in academia and industry alike, including mission-critical sectors FAA (Federal Aviation Administration), CERN (European Organization for Nuclear Research), and  WPPT (Wind Power Prediction Tool, ). However, applying traditional software analysis methods to assure safety and security of floating-point software is tremendously difficult, due to their large scale and semantic complexity. I will present two lines of approaches that address this challenge.  

 

(1) The first line is to reduce the problem of verifying/testing a program to minimizing a derived weak-distance function, which avoids static or symbolic reasoning about the program semantics. The approach has evolved into an floating-point satisfiability solver that performs hundreds of times faster than Microsoft's Z3 and MathSAT, and a coverage-based testing tool that outperformed Google's security-oriented fuzz tester AFL by 18% of branches on Oracle's math library.

 

(2) The other line of work is based on program transformation and fuzzing techniques. It detects many failures in the Robot Operating System and GNU Scientific Library.

 

Short bio:

Zhoulai Fu is an Assistant Professor in Computer Science at IT University of Copenhagen, Denmark.  Previously, he was a postdoc at UC Davis. He received his PhD from INRIA, France, and was a visiting scholar at IMDEA, Spain.  His research is published in top venues in Programming Languages (e.g. PLDI, POPL, CAV, OOPSLA, ICSE), spanning the fields of abstract interpretation, floating-point error analysis, formal verification and automated testing.

Computed Event Type: 
Mis