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.