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

CoqPL-2020-papers
15:35 - 17:45: CoqPL - Contributed Talks & Coq Developers at Maurepas
Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology
CoqPL-2020-papers15:35 - 16:05
Talk
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA
File Attached
CoqPL-2020-papers16:05 - 16:35
Talk
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
CoqPL-2020-papers16:35 - 16:50
Break
CoqPL-2020-papers16:50 - 17:35
Demonstration