Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore formal verification techniques for finding security vulnerabilities in JavaScript engines through this conference talk from Nullcon Berlin 2025. Discover how formal methods can be applied to analyze V8's C++ codebase, specifically focusing on the type analysis and range analysis components of the new Turboshaft JIT engine. Learn about the sophisticated optimization techniques JavaScript engines use to accelerate code execution and understand why bugs in these analysis systems have historically led to significant security issues. Examine the practical application of the ESBMC model checker for scrutinizing V8's range analysis functions and understand how to define correctness criteria for complex compiler optimizations. Master the setup process for bounded model checking of V8's C++ code and learn techniques for automatically generating JavaScript test cases that can demonstrate the existence of discovered bugs. Gain insights into the speaker's methodology for formal verification of compiler components and see a real-world example of how this approach successfully identified a previously unknown bug in V8's division operator implementation.
