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.
