We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in Linear Temporal Logic over Finite Traces (LTLf), interpreting them as symbolic finite automata (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of symbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures implicit in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.

翻译：本文提出了一种针对与带副作用的不透明库交互的函数式程序的符号执行（SE）过程。我们的过程允许以有限迹上的线性时序逻辑（LTLf）表达库和抽象数据类型（ADT）方法的规约，并将其解释为符号有限自动机（SFAs），从而在此环境下实现智能的规约引导路径探索。我们应用该技术来辅助证伪涉及ADT方法对底层不透明表示类型执行带副作用操作的复杂数据结构安全性质。规约自然地刻画了ADT方法（及其所依赖的库方法）允许执行的、按时间顺序排列的事件迹的容许集合。我们展示了如何利用这些规约为对应方法构造可行的符号输入状态，以及如何基于此形式化体系编码安全性质。更重要的是，我们引入了符号导数的概念，该机制允许SE过程基于所提供规约中隐含的自动机结构以及待证伪的安全性质，智能地欠近似其需要探索的前置条件状态集合。直观上，导数使符号执行能够利用基于迹的规约所定义的时间约束，快速剪除无果的路径并发现可行的错误状态。在多种具有挑战性的ADT实现上的实验结果表明了我们方法的有效性。