BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Model checking: Neural Termination Analysis - Dani
 el Kroening (Amazon Web Services)
DTSTART;TZID=Europe/London:20220722T141500
DTEND;TZID=Europe/London:20220722T150000
UID:TALK176270AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/176270
DESCRIPTION:We introduce a novel approach to the automated ter
 mination analysis of computer programs: we train n
 eural networks to behave as ranking functions. Ran
 king functions map program states to values that a
 re bounded from below and decrease as the program 
 runs. &nbsp\;The existence of a ranking function p
 roves that the program terminates. &nbsp\;We learn
  ranking functions from execution traces by traini
 ng a neural network so that its output decreases a
 long the sampled executions\; then\, we use symbol
 ic reasoning to formally verify that it generalise
 s to all possible executions. &nbsp\;We demonstrat
 e that\, thanks to the ability of neural networks 
 to represent highly complex functions\, our method
  succeeds over programs that are beyond the reach 
 of state-of-the-art tools. &nbsp\;This includes pr
 ograms that use loop guards with disjunctions and 
 programs that exhibit nonlinear behaviour.&nbsp\;
LOCATION:Seminar Room 2\, Newton Institute
CONTACT:
END:VEVENT
END:VCALENDAR