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）方法的规约，并将其解释为符号有限自动机（SFA），从而在此设置下实现智能的规约引导路径探索。我们应用该技术来促进基于ADT方法对底层不透明表示类型执行的副作用操作，对复杂数据结构安全属性进行证伪。规约自然地描述了ADT方法（以及它们所依赖的库方法）允许执行的时间顺序事件的可接受迹。我们展示了如何利用这些规约为相应方法构造可行的符号输入状态，以及如何基于此形式化体系对安全属性进行编码。更重要的是，我们引入了符号导数的概念，该机制允许SE过程基于所提供规约中隐含的自动机结构以及待证伪的安全属性，智能地欠近似其需要探索的前提条件状态集合。直观地说，导数使符号执行能够利用基于迹的规约所定义的时间约束，快速剪除无产出的路径并发现可行的错误状态。在大量具有挑战性的ADT实现上的实验结果证明了我们方法的有效性。