Fangzhen Lin from Hong Kong U of Science and Technology will be visiting next Tue, July 18, and give two talks on two extremely interesting and important works:

 1:30 PM: Verification---of our everyday programs using our everyday logic (making it even simple and fun to think about them)

 3:00 PM: Loop formulas---on building solvers for answer set programming problems (a fundamental result connecting two research areas).

Please see abstracts and a short bio below.

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.

Loops and Loop Formulas in Answer Set Programming

Answer set programming (ASP) is a constraint-based programming paradigm based on logic program with answer set semantics. In this talk, I will talk about my work (together with my students and collaborators) on loops and loop formulas: what they are and how they can be used in building ASP solvers.

Bio
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, logic programming, 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.