This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalise in Rocq. This method can be seen as a specialised induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviour by standard techniques.

Symbolic execution is a program analysis technique to systematically explore all possible paths through a program. The technique can be formally explained by means of small-step transition systems that update symbolic states and compute a precondition corresponding to the taken execution path. In stateful transition systems behavior may depend on previous transitions, which complicates compositional reasoning about programs. To enable compositonal reasoning this paper defines a denotational semantics for symbolic execution. The proposed semantics views a program as a set of traces, each of which has a corresponding substitution — the composition of all its assignments — and a corresponding path condition — the conjunction of all its Boolean tests under appropriate substitution. We prove correspondence between the symbolic denotational semantics and a concrete semantics. We argue that the symbolic denotational semantics is a very natural framework to reason about symbolic execution, and use it to prove that symbolic execution computes (weakest) preconditions. We provide mechanizations in Coq for the main results.