1 Problem: you have one program on one host and want to reproduce its execution on another host. They call it replay of application dialog. 2 You may have initiator, host A, and host B. Dialog is between initiator and A, initiator and B. They want to build post-condition q for program P such that it is true for output of host B with some modified host A input iff host B reproduces execution of host A. 3 So, this post-condition checks “similarity” of execution. But “similarity” may vary. Function Φ specifies what to check.

No image.

Program creates symbolic formula over state and input. They use this formula to check post-condition. They talk about forward symbolic execution with link to 1976 Symbolic execution and program testing. They said that if we symbolically execute all program paths, we could combine the formulas into a single formula for the entire program. But they want to compute the weakest pre-condition wp(P, q) that leads satisfying post-condition. Computing 4 includes translation program into GCL (guarded command language), computing formula and its simplifying.

Sergey Vartanov, 2007–2020