SPLASH 2019 (series) / VMIL 2019 (series) / VMIL 2019 /
Formal Verification of JIT by Symbolic Execution
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: Beirut change
Tue 22 Oct
Times are displayed in time zone: Beirut change
11:00 - 11:30 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 - 12:00 Full-paper | Efficient Fail-Fast Dynamic Subtype Checking VMIL Pre-print | ||
12:00 - 12:15 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 - 12:30 Talk | Formal Verification of JIT by Symbolic Execution VMIL Boris ShingarovLabWare |