Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 14-minute conference presentation from OOPSLA 2025 that introduces a novel formal reasoning system for composing heterogeneous program analyses. Learn about the challenges of soundly combining different analysis techniques in large software systems, where some components undergo full formal verification while others rely on testing or other under-approximated analysis methods. Discover how traditional compositional reasoning techniques like rely-guarantee reasoning work effectively for verified components but fail to handle components analyzed through testing or other under-approximated approaches.
Examine the paper's core contribution: a formal logical foundation called LabelBI based on the logic of bunched implications that enables rely-guarantee reasoning for systems with differently analyzed components. Understand how the approach models systems as collections of communicating processes, where each process owns internal resources and communicates through channels. Investigate the key concept of "test levels" that quantify behavioral guarantees by capturing the constraints under which these guarantees hold true.
Delve into the technical details of the LabelBI proof system and its trace semantics, including soundness proofs and cut elimination properties of the sequent calculus. Follow along with a practical case study demonstrating the logic's expressiveness in real-world scenarios. Access supplementary materials including the full research paper, artifact repository with reusable implementations, and reproducible results that have been peer-reviewed and validated by the conference's artifact evaluation process.
