The talk “smtgcc: Using an SMT solver to find bugs in GCC” will be presented by Krister Walfridsson on December the 4th, at 16:00, online:
Join the meeting
Meeting ID: 373 912 942 228 7
Passcode: XS9M8dT3
Abstract:
“SMT solvers are increasingly effective for finding compiler bugs and validating optimizations. This talk presents smtgcc, a translation-validation tool for GCC. It is similar to Alive2 for LLVM, but smtgcc’s approach diverges from Alive2 because GCC and LLVM follow different design choices. I will explain how smtgcc works and discuss issues in formalizing the semantics of GIMPLE, GCC’s IR.”
About the Speaker:
Krister Walfridsson became involved with the GCC project while studying at university in the mid-1990s. Since completing his studies, he has worked with both compilers and operating systems in various embedded environments. Most recently, he spent 10 years at Arm as a principal compiler engineer in the Mali GPU team. He is currently taking a few years off to work on personal projects and to dance.