Hoare Logic For Arm Machine Code
FSEN'07: Proceedings of the 2007 international conference on Fundamentals of software engineering(2007)
摘要
This paper shows how a machine-code Hoare logic is used to lift reasoning from the tedious operational model of a machine language to a manageable level of abstraction without making simplifying assumptions. A Hoare logic is placed on top of a high-fidelity model of the ARM instruction set. We show how the generality of ARM instructions is captured by specifications in the logic and how the logic can be used to prove loops and procedures that traverse pointer-based data structures. The presented work has been mechanised in the HOL4 theorem prover and is currently being used to verify ARM machine code implementations of arithmetic and cryptographic operations.
更多查看译文
关键词
Recursive Call, Program Counter, Machine Code, Separation Logic, Hoare Logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络