Compositional Symbolic Execution

We develop the theory and practice of compositional symbolic execution (CSE) – a technique that combines separation logic with symbolic execution to enable modular, scalable program analysis. A key theme of our work is establishing rigorous formal foundations that are faithfully reflected in tool implementations. We have introduced a formal CSE engine grounded in separation logic that provides a unified foundation for both correctness and incorrectness reasoning, with the two differing only in the choice between satisfiability and validity (ECOOP’24). This engine characterises the consume-produce technique used by tools such as VeriFast, Viper, and our own Gillian platform, and has enabled Gillian to support automatic true bug-finding via incorrectness bi-abduction. We have further extended this foundation to be parametric on the memory model, addressing the lack of a satisfactory formal basis for memory-model-parametric CSE platforms and covering models for C, JavaScript, and CHERI (OOPSLA’25).