Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 20-minute conference talk from POPL 2025 that presents a novel approach to symbolic execution for functional programs interacting with effectful, opaque libraries. The presentation, delivered by researchers from Purdue University, introduces a technique that uses Linear Temporal Logic over Finite Traces (LTLf) to express library and abstract data type specifications, interpreting them as symbolic finite automata to enable intelligent specification-guided path exploration. Learn how this approach facilitates the falsification of complex data structure safety properties through the innovative use of symbolic derivatives—a mechanism that allows symbolic execution to underapproximate precondition states based on automata structures in specifications. The talk demonstrates how derivatives help prune unproductive paths and discover feasible error states efficiently, with experimental results showing effectiveness across challenging ADT implementations. The research includes available and reusable artifacts accessible through the provided Zenodo link.
