Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Tue 22 Oct 2019 12:15 - 12:30 at Abbey - Session #2 Chair(s): Anthony Canino

This work-in-progress report presents ongoing experiments relating to formal verification of JIT compilers for language VMs. The native CPU code of the VM — which consists of statically-known code and variable output of the JIT — is executed in a symbolic simulation engine. This simulation yields identities that hold over the total range of inputs (or disproves them by providing a counterexample).

One obstacle we had to overcome, is executing CPU code which is itself symbolic, i.e. given as formulae over input variables. To solve this problem, we designed a new ISA-agnostic translator from ISA-specific binary machine language into an intermediate language which can be directly simulated by the symbolic engine.

Tue 22 Oct
Times are displayed in time zone: (GMT+03:00) Beirut change

11:00 - 12:30: Session #2VMIL at Abbey
Chair(s): Anthony CaninoSUNY Binghamton
11:00 - 11:30
Full-paper
VMIL
Isaac Oscar GarianoVictoria University of Wellington, Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington
11:30 - 12:00
Full-paper
VMIL
Rohan PadhyeUniversity of California, Berkeley, Koushik SenUniversity of California, Berkeley
Pre-print
12:00 - 12:15
Talk
VMIL
Kiko Fernandez-ReyesUppsala University, Isaac Oscar GarianoVictoria University of Wellington, James NobleVictoria University of Wellington, Tobias WrigstadUppsala University
Pre-print
12:15 - 12:30
Talk
VMIL