IC Colloquium: Learning-aided Program Reasoning
Event details
| Date | 19.03.2020 |
| Hour | 13:00 › 14:00 |
| Category | Conferences - Seminars |
The talk will take place via zoom. Please click on the following link: https://epfl.zoom.us/j/598929700
By: Xujie Si - University of Pennsylvania
IC Faculty candidate
Abstract:
The enormous rise in the scale, scope, and complexity of software has led to widespread interest in program reasoning tools. Despite broad adoption by industry, developing such tools remains challenging. Their designers must carefully customize heuristics or analysis rules for each codebase in order to achieve a usable accuracy and scalability. Moreover, their users often have to provide correct annotations and inspect a large number of reports. Furthermore, the slow feedback cycle between users and designers hinders the usability of these reasoning tools in the modern software CI/CD cycle. Can program reasoning algorithms be effectively learned and automatically improved over time?
In this talk, I will show how to equip discrete logical reasoning with learning capability by exploiting continuous numerical reasoning. I will first present a framework that combines probabilistic reasoning with logical reasoning. This general framework enables learning logical rules for many applications including program analysis, which significantly alleviates the burden on analysis designers, and recommending most relevant alarms based on user feedback as well as code changes, which significantly reduces the manual effort of investigating alarms.
Secondly, 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 software verification. Compared to state-of-the-art approaches, Code2Inv requires orders of magnitude fewer queries to the underlying checker and generates more natural loop invariants.
I will conclude by describing how learning-based techniques promise to enable the next generation of intelligent programming systems, with applications in diverse areas such as software analysis and testing, algorithm synthesis, proof automation, differentiable programming, and neuro-symbolic reasoning.
Bio:
Xujie Si is a Ph.D. candidate at the University of Pennsylvania, advised by Mayur Naik.
His research spans programming languages, software engineering, security, and artificial intelligence. He is interested in developing learning-based techniques to help programmers build better software with less effort. He has developed systems that automatically learn API specifications from massive codebases, improve the accuracy of static analysis by learning from a small amount of user feedback, and learn to verify programs without requiring any human annotations. He is a recipient of the 2019 PLDI Distinguished Paper Award.
More information
By: Xujie Si - University of Pennsylvania
IC Faculty candidate
Abstract:
The enormous rise in the scale, scope, and complexity of software has led to widespread interest in program reasoning tools. Despite broad adoption by industry, developing such tools remains challenging. Their designers must carefully customize heuristics or analysis rules for each codebase in order to achieve a usable accuracy and scalability. Moreover, their users often have to provide correct annotations and inspect a large number of reports. Furthermore, the slow feedback cycle between users and designers hinders the usability of these reasoning tools in the modern software CI/CD cycle. Can program reasoning algorithms be effectively learned and automatically improved over time?
In this talk, I will show how to equip discrete logical reasoning with learning capability by exploiting continuous numerical reasoning. I will first present a framework that combines probabilistic reasoning with logical reasoning. This general framework enables learning logical rules for many applications including program analysis, which significantly alleviates the burden on analysis designers, and recommending most relevant alarms based on user feedback as well as code changes, which significantly reduces the manual effort of investigating alarms.
Secondly, 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 software verification. Compared to state-of-the-art approaches, Code2Inv requires orders of magnitude fewer queries to the underlying checker and generates more natural loop invariants.
I will conclude by describing how learning-based techniques promise to enable the next generation of intelligent programming systems, with applications in diverse areas such as software analysis and testing, algorithm synthesis, proof automation, differentiable programming, and neuro-symbolic reasoning.
Bio:
Xujie Si is a Ph.D. candidate at the University of Pennsylvania, advised by Mayur Naik.
His research spans programming languages, software engineering, security, and artificial intelligence. He is interested in developing learning-based techniques to help programmers build better software with less effort. He has developed systems that automatically learn API specifications from massive codebases, improve the accuracy of static analysis by learning from a small amount of user feedback, and learn to verify programs without requiring any human annotations. He is a recipient of the 2019 PLDI Distinguished Paper Award.
More information
Practical information
- General public
- Free
- This event is internal