Learning to Verify the Heap
Event details
| Date | 02.06.2016 |
| Hour | 14:00 › 15:30 |
| Location | |
| Category | Conferences - Seminars |
by Siddharth Krishna
Abstract
We present a data-driven verification framework to automatically prove memory safety and functional correctness of heap programs. For this, we introduce a novel statistical machine learning technique that maps observed program states to (possibly disjunctive) separation logic formulas describing the invariant shape of data structures at relevant program locations. We then attempt to verify these predictions using a theorem prover, where counterexamples to a predicted invariant are used as additional input to the shape predictor in a refinement loop. After obtaining valid shape invariants, we use a second learning algorithm to strengthen them with data invariants, again employing a refinement loop using the underlying theorem prover.
We have implemented our techniques in Cricket, an extension of the GRASShopper verification tool. Cricket is able to automatically prove memory safety and correctness of implementations of a variety of classical list-manipulating algorithms such as insertionsort.
This is joint work with Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Daniel Tarlow, and He Zhu.
Bio
Siddharth Krishna is a PhD student in the Computer Science Department of New York University, who works with Thomas Wies. He is interested in using Machine Learning for program verification and synthesis, and on using SMT and local theories to verify heap manipulating programs.
More information
Abstract
We present a data-driven verification framework to automatically prove memory safety and functional correctness of heap programs. For this, we introduce a novel statistical machine learning technique that maps observed program states to (possibly disjunctive) separation logic formulas describing the invariant shape of data structures at relevant program locations. We then attempt to verify these predictions using a theorem prover, where counterexamples to a predicted invariant are used as additional input to the shape predictor in a refinement loop. After obtaining valid shape invariants, we use a second learning algorithm to strengthen them with data invariants, again employing a refinement loop using the underlying theorem prover.
We have implemented our techniques in Cricket, an extension of the GRASShopper verification tool. Cricket is able to automatically prove memory safety and correctness of implementations of a variety of classical list-manipulating algorithms such as insertionsort.
This is joint work with Marc Brockschmidt, Yuxin Chen, Byron Cook, Pushmeet Kohli, Daniel Tarlow, and He Zhu.
Bio
Siddharth Krishna is a PhD student in the Computer Science Department of New York University, who works with Thomas Wies. He is interested in using Machine Learning for program verification and synthesis, and on using SMT and local theories to verify heap manipulating programs.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Viktor Kuncak