Center for Global Studies

View Full Calendar

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
wifi event
Date
Feb 9, 2024   2:00 pm  
Speaker
Hrishikesh Balakrishnan, UIUC
Contact
Isha Chaudhary
E-Mail
isha4@illinois.edu
Views
90
Originating Calendar
Siebel School Speakers Calendar

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.

link for robots only