Inference of Robust Reachability Constraints

Explore a 19-minute video presentation from POPL 2024 conference that introduces an innovative approach to characterizing bugs and attack vectors in software systems. Learn about the concept of robust reachability and its extension using theory-agnostic abduction techniques to generate constraints on uncontrolled program inputs. Discover how this method improves upon previous approaches by addressing mostly reproducible violations and providing high-level feedback for program violation characterization. Examine the implementation's practical application in vulnerability characterization for fault injection attacks and its evaluation on standard benchmarks from software verification and security analysis. Gain insights into the complete and efficient exploration of the inference space, and understand how this advancement contributes to the development of more sophisticated verification tools.

[POPL'24] Inference of Robust Reachability Constraints