FO-Complete Program Verification for Heap Logics
We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. The logics we develop are a frame logic (FL) and a separation logic that has an alternate semantics inspired by frame logic, SL-FL. We show verification condition generation for FL that are amenable to FO-complete reasoning that combines quantifier instantiation and SMT solvers. We show SL-FL can be translated to FL in order to obtain FO-complete reasoning. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures.
Sat 18 OctDisplayed time zone: Perth change
10:30 - 12:15 | |||
10:30 15mTalk | FO-Complete Program Verification for Heap Logics OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Hrishikesh Balakrishnan University of Illinois Urbana-Champaign, Aaron Councilman Univ of Illinois Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
10:45 15mTalk | Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back OOPSLA Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Francesca Randone Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy, Tobias Winkler RWTH Aachen University | ||
11:00 15mTalk | Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models OOPSLA Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
11:45 15mTalk | Scaling Instruction-Selection Verification against Authoritative ISA Semantics OOPSLA Michael McLoughlin Carnegie Mellon University, Ashley Sheng Wellesley College, Chris Fallin F5, Bryan Parno Carnegie Mellon University, Fraser Brown CMU, Alexa VanHattum Wellesley College DOI | ||
12:00 15mTalk | Verification of Bit-Flip Attacks against Quantized Neural Networks OOPSLA Yedi Zhang National University of Singapore, Lei Huang ShanghaiTech University, Pengfei Gao ByteDance, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||