An Abstract, Approximation-Based Approach to Embedded Code Pointers and Partial-Correctness

To support higher-order type-like features such as embedded code pointers in logic-based verification, one approach is to build a syntactic assertion logic that combines logic and types. But it is not totally satisfactory in various aspects. Another approach is to use approximation to simulate the behavior of types and typing invariants in logic, but this pollutes program specifications and proofs with complex approximation details. Additionally, existing approximation-based work supports embedded code pointers without partial-correctness guarantee.

We propose a new abstract, approximation-based approach to support embedded code pointers in logic-based verification. Our specification language and inference rules are independent of approximation, thus allowing programs to be certified abstractly. For the support of embedded code pointers, this benefits not only interactive-verification, but certifying compilation and automated theorem proving as well. Approximation is only used to establish soundness and partial-correctness. This proves to be advantageous for meta theory design and mechanizing. Additionally, we easily support dynamic code generation. The central idea should be applicable to other higher-order features. Our work is presented on and mechanized in, but not limited to, assembly languages and the Coq proof-assistant.