Amsterdam/Saarbrücken/Munich, 21 June 2018. Solid Sands, the supplier of SuperTest, the industry-leading and largest test and validation suite for C and C++ compilers and libraries, and AbsInt, the specialist for program analysis tools for safety-critical software, today announce their collaboration to develop and integrate the SuperTest qualification suite into the C qualification support kit of the formally verified CompCert compiler.
The SuperTest qualification suite is derived from the established SuperTest compiler test and validation suite. It is tailored to the needs of AbsInt to fit the CompCert C qualification support kit. The close collaboration between AbsInt and Solid Sands allows customers to qualify their specific use case of the CompCert C compiler for qualification standards such as ISO 26262, IEC 61508, EN 50128, DO-333 and DO-330.
“I’m very proud that AbsInt has chosen to work with Solid Sands on CompCert’s Qualification Kit for two reasons,” said Marcel Beemster, Solid Sands CTO. “One, I am a long time admirer of AbsInt’s strong heritage in applying scientific methods to practical software engineering. Second, it was my university teacher Peter van Emde Boas who was the recipient of Donald Knuth’s letter (PDF) with the famous quote “Beware of bugs in the above code; I have only proved it correct, not tried it”, and this fits so well with the combination of CompCert’s foundation in formal methods and SuperTest’s ever improving test suite.”
“Does it make sense to test a formally verified compiler? While we do not expect to find bugs in the formally verified CompCert implementation, SuperTest brings confidence that the formal semantics of C, on which CompCert’s correctness proof is based, is indeed correct.” said Christian Ferdinand, AbsInt CEO. “Qualification requires testing according to common safety standards. SuperTest fits our needs very well and is easy to use and adapt.”
About AbsInt
AbsInt provides unique tools and services for the development, analysis, validation, verification, and certification of safety-critical software. The company name is an acronym for “abstract interpretation”, a sophisticated approach to static program analysis on which many of the company’s highly successful products are based. Founded in 1998, AbsInt is a privately-held company in Saarbrücken, Germany.
For further information, visit www.absint.com.
About Solid Sands
Solids Sands is the one-stop shop for C and C++ compiler and library testing, validation and safety services. With SuperTest, it offers the largest test and validation suite with a unique level of compiler and library test coverage. SuperTest starts where other suites end, enabling its users to achieve the software quality level required by ISO standards.
More information on Solid Sands is available at www.solidsands.nl. You can also follow them on LinkedIn and Twitter.
Press contacts
Marianne Damstra, Solid Sands
marianne@solidsands.nl
Sylvie Tritz, AbsInt
tritz@absint.com