A palestra “smtgcc: Using an SMT solver to find bugs in GCC” será apresentada por Krister Walfridsson no dia 4 de dezembro, às 16:00, online:
Join the meeting
Meeting ID: 373 912 942 228 7
Passcode: XS9M8dT3
Resumo:
“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.”
Sobre o Palestrante:
Krister Walfridsson envolveu-se no projeto GCC enquanto estudante universitário, em meados da década de 1990. Desde que concluiu os estudos, trabalhou com compiladores e sistemas operacionais em vários ambientes incorporados. Mais recentemente, passou 10 anos na Arm como Principal Engineer na equipa Mali GPU. Atualmente, está a tirar alguns anos de pausa para se dedicar a projetos pessoais e à dança.