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

vmil-2019-papers
11:00 - 12:30: VMIL 2019 - Session #2 at Abbey
Chair(s): Anthony CaninoSUNY Binghamton
vmil-2019-papers11:00 - 11:30
Full-paper
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
vmil-2019-papers11:30 - 12:00
Full-paper
Rohan PadhyeUniversity of California, Berkeley, Koushik SenUniversity of California, Berkeley
Pre-print
vmil-2019-papers12:00 - 12:15
Talk
Kiko Fernandez-ReyesUppsala University, Isaac Oscar GarianoVictoria University of Wellington, James NobleVictoria University of Wellington, Tobias WrigstadUppsala University
Pre-print
vmil-2019-papers12:15 - 12:30
Talk