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.
School of Computing and Data Science
Thomas M. Siebel Center for Computer Science201 N. Goodwin Ave. MC-258Urbana, IL 61801
Chicago Office200 South Wacker Drive, Suite 701 Chicago, IL 60606
General email: admin@siebelschool.illinois.edu