Specification-Driven Generation of Summaries for Symbolic Execution (Extended Version)

Symbolic execution is a popular program analysis technique that has been successfully used for bug-finding and bounded verification in various modern programming languages. Despite its popularity, however, symbolic execution suffers from two main limitations when applied to real-world code: interactions with the runtime environment and path explosion. Symbolic summaries are the standard solution to tackle these challenges. Yet, the development of summaries remains to this day a manual task that is known to be highly error-prone. To address this, we propose SumGen, a new tool for automatically generating correct-by-construction summaries from function specifications. With SumGen, we were able to generate a total of 131 summaries for 47 LIBC functions, demonstrating the effectiveness of our methodology in producing correct summaries for real-world, highly complex code. This is an extended version of a paper accepted into ESOP 2026. It is essentially identical to that paper, except that it includes appendices with evidence supporting the claims made in the paper. However, it does not incorporate changes (if any) made by the publisher, and is not the Version of Record.