AI, Data Science & Cloud Certificates from Google, IBM & Meta — 40% Off
One plan covers every Professional Certificate on Coursera. 40% off Coursera Plus Annual.
Unlock All Certificates
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.
