Hrishikesh Balakrishnan "FO-Complete Program Verification for Frame Logic"
- Event Type
- Seminar/Symposium
- Sponsor
- Illinois Computer Science
- Location
- 3401 Siebel Center for Computer Science
- Virtual
- Join online
- Date
- Feb 9, 2024 2:00 pm
- Speaker
- Hrishikesh Balakrishnan, UIUC
- Contact
- Isha Chaudhary
- isha4@illinois.edu
- Views
- 257
We look forward to seeing you in person (3401 Siebel Center for Computer Science) or online on Friday, February 9.
Abstract: Frame Logic is a logic for specifying properties of heap manipulating programs based on first-order logic with recursive definitions (FORD) that has a support operator akin to implicit heaplets in separation logic. I will present (1) an FO-complete automatic verification technique for programs annotated with frame logic specifications using a novel verification condition generation followed by reasoning in FORD using the technique of natural proofs. (2) A separation logic with alternate semantics that can be converted to frame logic to realize FO-complete program reasoning.