Abstract 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.

Despite the large number of partial reference implementations of the JavaScript language, there is currently no automatic mechanism for selecting the appropriate official tests for such implementations. To fill this gap, we introduce a new format for presenting the metadata associated with the tests included in Test262, the official JavaScript test suite, and present MetaData262, a new tool for both computing the metadata of Test262 tests and filtering tests according to their respective metadata properties.