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.

Conference Day
Tue 22 Oct

Displayed time zone: Beirut change

11:00 - 12:30
Session #2VMIL at Abbey
Chair(s): Anthony CaninoSUNY Binghamton
11:00
30m
Full-paper
Which of my Transient Type Checks are not (Almost) Free?
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
30m
Full-paper
Efficient Fail-Fast Dynamic Subtype Checking
VMIL
Rohan PadhyeUniversity of California, Berkeley, Koushik SenUniversity of California, Berkeley
Pre-print
12:00
15m
Talk
Towards Gradual Checking of Reference Capabilities
VMIL
Kiko Fernandez-ReyesUppsala University, Isaac Oscar GarianoVictoria University of Wellington, James NobleVictoria University of Wellington, Tobias WrigstadUppsala University
Pre-print
12:15
15m
Talk
Formal Verification of JIT by Symbolic Execution
VMIL