Verified just-in-time compiler on x86

DOI10.1145/1706299.1706313zbMath1312.68046OpenAlexW2001154106MaRDI QIDQ5255066

Magnus O. Myreen

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706313

zbMATH Keywords

compiler verificationjust in timeself-modifying code

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it), Verified abstract interpretation techniques for disassembling low-level self-modifying code, Function extraction, A Verified Runtime for a Verified Theorem Prover, Unveiling metamorphism by abstract interpretation of code properties

Uses Software

• HOL