Sciweavers

AMAST
2008
Springer

Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving

14 years 2 months ago
Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving
Abstract. Vx86 is the first static analyzer for sequential Intel x86 assembler code using automated deductive verification. It proves the correctness of assembler code against function contracts, which are expressed in terms of pre-, post-, and frame conditions using first-order predicates. Vx86 takes the annotated assembler code, translates it into C code simulating the processor, and then uses an existing C verifier to either prove the correctness of the assembler program or find errors in it. First experiments on applying Vx86 on the Windows Hypervisor code base are encouraging. Vx86 verified the Windows Hypervisor's memory safety, arithmetic safety, call safety and interrupt safety.
Stefan Maus, Michal Moskal, Wolfram Schulte
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AMAST
Authors Stefan Maus, Michal Moskal, Wolfram Schulte
Comments (0)