22 July 2019 - Fangzhen Lin (The Hong Kong University of Science and Technology) Abstract In this talk, Fangzhen Lin will describe a recent work of his on translating computer programs to first-order theories with quantification over natural numbers. The key ideas are to use inductive definitions to capture the behaviour of a loop, and to use a natural number constant to explicitly represent the number of iterations that a loop need to execute before terminating. They have implemented this translation for programs with loops and arrays, and made it into a program verification system using some off-the-shelf tools such as SymPy (an open source symbolic mathematics system), and Z3 (an SMT solver from Microsoft Research). We have entered our system, called VIAP (a Verifier for Integer Assignment Programs), at SV-COMP 2018 and SV-COMP 2019. It came out first in the ReachSafety-Arrays and ReachSafety-Recursive sub-categories of the ReachSafety category at SV-COMP 2019. In particular, their system has been able to verify some non-trivial programs without the the need of user-provided loop invariants. Biography Fangzhen Lin is a Professor at the Hong Kong University of Science and Technology, and the director of the HKUST-Xiaoi Robot joint lab. He received his PhD degree in computer science from Stanford University, and is a Fellow of AAAI. He 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-2006, 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 2019 Survey Track, IJCAI 2015 KR Track, KR 2010 and LPNMR'09. Jul 22 2019 14.00 - 15.00 22 July 2019 - Fangzhen Lin (The Hong Kong University of Science and Technology) Program Verification in First-Order Logic IF 4.31/33
22 July 2019 - Fangzhen Lin (The Hong Kong University of Science and Technology) Abstract In this talk, Fangzhen Lin will describe a recent work of his on translating computer programs to first-order theories with quantification over natural numbers. The key ideas are to use inductive definitions to capture the behaviour of a loop, and to use a natural number constant to explicitly represent the number of iterations that a loop need to execute before terminating. They have implemented this translation for programs with loops and arrays, and made it into a program verification system using some off-the-shelf tools such as SymPy (an open source symbolic mathematics system), and Z3 (an SMT solver from Microsoft Research). We have entered our system, called VIAP (a Verifier for Integer Assignment Programs), at SV-COMP 2018 and SV-COMP 2019. It came out first in the ReachSafety-Arrays and ReachSafety-Recursive sub-categories of the ReachSafety category at SV-COMP 2019. In particular, their system has been able to verify some non-trivial programs without the the need of user-provided loop invariants. Biography Fangzhen Lin is a Professor at the Hong Kong University of Science and Technology, and the director of the HKUST-Xiaoi Robot joint lab. He received his PhD degree in computer science from Stanford University, and is a Fellow of AAAI. He 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-2006, 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 2019 Survey Track, IJCAI 2015 KR Track, KR 2010 and LPNMR'09. Jul 22 2019 14.00 - 15.00 22 July 2019 - Fangzhen Lin (The Hong Kong University of Science and Technology) Program Verification in First-Order Logic IF 4.31/33
Jul 22 2019 14.00 - 15.00 22 July 2019 - Fangzhen Lin (The Hong Kong University of Science and Technology) Program Verification in First-Order Logic
