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
|11:00 - 11:30|
|11:30 - 12:00|
|12:00 - 12:15|
Kiko Fernandez-ReyesUppsala University, Isaac Oscar GarianoVictoria University of Wellington, James NobleVictoria University of Wellington, Tobias WrigstadUppsala UniversityPre-print
|12:15 - 12:30|