: Fangzhen Lin
, Hong Kong University of Science and Technology
Title: Program Verification in First-Order Logic
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), Wolfram Mathematica, 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.
Fangzhen Lin is a Professor in the Department of Computer Science and Engineering at the Hong Kong University of Science and Technology. He is interested in AI, particularly in Knowledge Representation and Reasoning, and currently has related projects in computer program verification, game theory, and social choice theory. He received his PhD degree in computer science from Stanford University.
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. He had served as Associate Editor of Artificial Intelligence and Journal of AI Research, and was program co-chairs of IJCAI 2015 KR Track, KR 2010 and LPNMR'09.