BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Learning-aided Program Reasoning
DTSTART:20200319T130000
DTEND:20200319T140000
DTSTAMP:20260407T043352Z
UID:e927d8c0890c69690733b1781e0ecb4ec959b740e31b2a4f59b4ded5
CATEGORIES:Conferences - Seminars
DESCRIPTION:The talk will take place via zoom. Please click on the followi
 ng link: https://epfl.zoom.us/j/598929700 \n\nBy: Xujie Si - University o
 f Pennsylvania\nIC Faculty candidate\n\nAbstract:\nThe enormous rise in th
 e scale\, scope\, and complexity of software has led to widespread interes
 t in program reasoning tools. Despite broad adoption by industry\, develo
 ping such tools remains challenging. Their designers must carefully custom
 ize heuristics or analysis rules for each codebase in order to achieve a 
 usable accuracy and scalability. Moreover\, their users often have to prov
 ide correct annotations and inspect a large number of reports. Furthermor
 e\, the slow feedback cycle between users and designers hinders the usabi
 lity of these reasoning tools in the modern software CI/CD cycle. Can prog
 ram reasoning algorithms be effectively learned and automatically improve
 d over time?\n\nIn this talk\, I will show how to equip discrete logical r
 easoning with learning capability by exploiting continuous numerical reaso
 ning. I will first present a framework that combines probabilistic reason
 ing with logical reasoning. This general framework enables learning logic
 al rules for many applications including program analysis\, which signific
 antly alleviates the burden on analysis designers\, and recommending most
  relevant alarms based on user feedback as well as code changes\, which si
 gnificantly reduces the manual effort of investigating alarms. \n\nSecon
 dly\, as a complement to bug detection\, I will present an end-to-end deep
  reinforcement learning framework\, Code2Inv\, which automatically learns
  to generate loop invariants\, a fundamental challenge in automated softwa
 re verification. Compared to state-of-the-art approaches\, Code2Inv requir
 es orders of magnitude fewer queries to the underlying checker and generat
 es more natural loop invariants. \n\nI will conclude by describing how l
 earning-based techniques promise to enable the next generation of intellig
 ent programming systems\, with applications in diverse areas such as soft
 ware analysis and testing\, algorithm synthesis\, proof automation\, diffe
 rentiable programming\, and neuro-symbolic reasoning.\n\nBio:\nXujie Si i
 s a Ph.D. candidate at the University of Pennsylvania\, advised by Mayur N
 aik.\nHis research spans programming languages\, software engineering\, se
 curity\, and artificial intelligence. He is interested in developing lear
 ning-based techniques to help programmers build better software with less 
 effort. He has developed systems that automatically learn API specificati
 ons from massive codebases\, improve the accuracy of static analysis by le
 arning from a small amount of user feedback\, and learn to verify program
 s without requiring any human annotations. He is a recipient of the 2019 P
 LDI Distinguished Paper Award.\n\nMore information
LOCATION:
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR