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
11:00 - 12:30
|Which of my Transient Type Checks are not (Almost) Free?|
|Efficient Fail-Fast Dynamic Subtype Checking|
|Towards Gradual Checking of Reference Capabilities|
Kiko Fernandez-ReyesUppsala University, Isaac Oscar GarianoVictoria University of Wellington, James NobleVictoria University of Wellington, Tobias WrigstadUppsala UniversityPre-print
|Formal Verification of JIT by Symbolic Execution|