BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Date iCal//NONSGML kigkonsult.se iCalcreator 2.20.2//
METHOD:PUBLISH
X-WR-CALNAME;VALUE=TEXT:Eventi DIAG
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:STANDARD
DTSTART:20181028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20180325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:calendar.13484.field_data.0@oba.diag.uniroma1.it
DTSTAMP:20260407T080455Z
CREATED:20180606T110537Z
DESCRIPTION:Computer programs are among the most complex man-made systems. 
  Given their widespread uses\, many of them in critical applications\, the
 ir reliability is of utmost importance. There have been many formalisms an
 d methods proposed for reasoning about computer programs\, and many techni
 ques and methodologies for designing and debugging programs. In this talk\
 , I will first briefly review some of the existing approaches and then pre
 sent my recent work on translating computer programs to first-order logic 
 with quantification over natural numbers. We have implemented this transla
 tion for programs with loops and arrays\, and made it into a program verif
 ication system using off-the-shelf tools such as SymPy (an open source sym
 bolic 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 shar
 e our experiences in constructing the system and discuss some extensions t
 hat we are working on. Bio Fangzhen LinDepartment of Computer ScienceThe H
 ong Kong University of Science and TechnologyClear Water Bay\, Kowloon\, H
 ong 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 Resea
 rch Fellowship award in 2006\, a Distinguished Paper Award at IJCAI-97\, a
  Best Paper Award at KR-2000\, an Outstanding Paper Honorable Mention at A
 AAI-04\, the Ray Reiter Best Paper award at KR-06\, and an Honorable Menti
 on for his planner R at the AIPS-2000 planning competition.
DTSTART;TZID=Europe/Paris:20180702T110000
DTEND;TZID=Europe/Paris:20180702T110000
LAST-MODIFIED:20191008T082902Z
LOCATION:B203
SUMMARY:Program Verification in First-Order Logic - Fangzhen Lin (Hong Kong
  Univ)  - Fangzhen Lin (Hong Kong University of Science and Technology)
URL;TYPE=URI:http://oba.diag.uniroma1.it/node/13484
END:VEVENT
END:VCALENDAR