Department of Computer, Control and Management Engineering

Computer programs are among the most complex man-made systems.  Given their widespread uses, many of them in critical applications, their reliability is of utmost importance. There have been many formalisms and methods proposed for reasoning about computer programs, and many techniques and methodologies for designing and debugging programs. In this talk, I will first briefly review some of the existing approaches and then present my recent work on translating computer programs to first-order logic with quantification over natural numbers. We have implemented this translation for programs with loops and arrays, and made it into a program verification system using off-the-shelf tools such as SymPy (an open source symbolic mathematics system),  and Z3 (an SMT solver from Microsoft Research). Our system can verify automatically some non-trivial benchmark programs that require user-provided loop invariants for other systems. I will share our experiences in constructing the system and discuss some extensions that we are working on. 

Bio

Fangzhen Lin
Department of Computer Science
The Hong Kong University of Science and Technology
Clear Water Bay, Kowloon, Hong Kong

Fangzhen Lin (PhD, Stanford) is a Professor in the Department of Computer Science at the Hong Kong University of Science and Technology.  He is a Fellow of AAAI, and received the Croucher Foundation Senior Research Fellowship award in 2006, a Distinguished Paper Award at IJCAI-97, a Best Paper Award at KR-2000, an Outstanding Paper Honorable Mention at AAAI-04, the Ray Reiter Best Paper award at KR-06, and an Honorable Mention for his planner R at the AIPS-2000 planning competition.