Historia: Refuting Callback Reachability with Message-History Logics

Explore a groundbreaking approach to addressing the callback reachability problem in event-driven programming frameworks through this 18-minute conference talk from OOPSLA2 2023. Delve into the innovative use of message-history logics to decouple the specification of callback control flow from app code analysis. Learn how the Historia verifier employs a targeted specification approach to prove the absence of multi-callback bug patterns in real-world Android apps. Discover the potential of this middle-ground solution that allows for gradual refinement of callback control flow to prove assertions of interest, offering a unique capability to distinguish between buggy and fixed versions in challenging real-world scenarios.