一句话：提出 DDSE，一种面向函数式语言的高阶需求驱动符号反向执行，证明其可靠性并用于测试生成。
符号反向执行（SBE）让符号求值可从程序任意位置开始并逆向执行到程序入口，从而支持目标导向推理，已在命令式语言的自动测试生成中展现实用性。本文提出 DDSE，一种面向函数式（而非命令式）语言的新型 SBE。DDSE 被定义为反向执行解释器的自然扩展，支持高阶特性，并采用需求驱动策略。作者形式化定义了 DDSE，建立其可靠性（soundness），并针对该玩具语言给出测试生成算法；还报告了一个初始参考实现，以验证设计原则的正确性。
Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages. In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.
@article{PalmerPSW20,
title = {Higher-order demand-driven symbolic evaluation},
author = {Zachary Palmer and Theodore Park and Scott Smith and Shiwei Weng},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408984}
}