Abstract Machine Supporting Bit Arithmetic Reasoning
Lin Chun-xiao · Mini-micro Systems · 2007
The gap between the physical machine and the abstract machine used in program reasoning reduces the accuracy of reasoning. In order to shorten this gap, a new abstract machine with bit-level abstraction is proposed, in which the binary integers are represented as bit vector in syntactic approach instead of non-negative integer number. With this new abstract machine, many programs with bit operation instructions, especially system-level codes, can be reasoned using Hoare Logic. In this paper, the binary integer along with its arithmetic and logic operations are formalized in Coqs Calculus of Inductive Construction, and many important properties are also formally proved in Coq proof assistant.