Active.
Symbolic execution has been an active area of research for almost 50 years. 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.
Zachary Palmer, Theodore Park, Scott Smith, Shiwei Weng, Higher-Order Demand-Driven Symbolic Evaluation, Proceedings of the ACM on Programming Languages, Volume 4, Number ICFP, Article 102 (August 2020), 28 pages. Artifact. Full paper. Slide.
In this paper we define DDSE: a demand- driven symbolic evaluator for higher-order functional languages which also propagates constraints backwards. DDSE is a novel SBE which operates on a functional as opposed to imperative language, and furthermore it is defined as a direct abstraction of a backwards-executing interpreter. This reverse propagation is similar in spirit to how Dijkstra weakest-preconditions (wps) are propagated, and how classic backward program analyses propagate constraints in reverse. The advantage of SBE is the same as any goal-directed reasoning: by focusing on the goal from the start, there are fewer spurious paths taken.
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.