Write a Blog >>

Just-in-Time compilation consists in interleaving program interpretation and compilation at run-time, to achieve better performance than standard interpretation. While some of the execution time is spent compiling, a JIT compiler can leverage run-time information to make speculative optimizations. These optimizations create optimized versions of functions given some assumptions. While static compilers have been the topic of many formal verification works, few have tackled JIT compilation verification. We present our ongoing work about formal verification of a Just-in-Time compiler.

slides_coqpl20 (pres.pdf)834KiB
(coqpl20-final5.pdf)360KiB

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

15:35 - 17:45: Contributed Talks & Coq DevelopersCoqPL at Maurepas
Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology
15:35 - 16:05
Talk
CoqPL
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA
File Attached
16:05 - 16:35
Talk
CoqPL
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA, Andrej DudenhefnerSaarland University, Edith HeiterSaarland University, Dominik KirstSaarland University, Fabian KunzeSaarland University, Gert SmolkaSaarland University, Simon SpiesSaarland University, Dominik WehrSaarland University, Universiteit van Amsterdam, Maximilian WuttkeSaarland University
Media Attached File Attached
16:35 - 16:50
Break
CoqPL
16:50 - 17:35
Demonstration
CoqPL