Room 206 (2nd floor, badged access)
7 November 2024 - 14h00
Formal Verification Beyond Traditional Compilation
by Aurèle Barrière from EPFL
Abstract: Modern dynamic programming language implementations often use compilation, but do so in atypical ways. In this talk, I focus on two concrete examples from dynamic languages implementations.
First, many dynamic language implementations use Just-in-Time (JIT) compilation for performance. JITs interleave the execution of a program, its optimizations, and native compilation. Many JITs also speculate on the programs they execute, and provide ways to deoptimize when speculation fails. I present a methodology to extend static compiler verification techniques to reason about JIT execution formally and develop verified JIT compilers in Coq.
Second, modern regex engines typically compile regexes to specific bytecodes that can be executed in different ways with different complexity. But regexes have changed a lot since traditional regular expressions, and modern engines suffer from semantic bugs and exponential complexity, even in cases where it could be avoided. I present our on-going effort to achieve linear-time and formally verified JavaScript regex engines. This involves designing new linear matching algorithms and new ways to formally reason about modern regexes.
