A Compositional Logic for Control Flow.

We present a program logic, , which modularly reasons about unstructured control flow in machine-language programs. Unlike previous program logics, the basic reasoning units in are multiple-entry and multiple-exit program fragments. provides fine-grained composition rules to compose program fragments. It is not only useful for reasoning about unstructured control flow in machine languages, but also useful for deriving rules for common control-flow structures such as while-loops, repeat-until-loops, and many others. We also present a semantics for and prove that the logic is both sound and complete with respect to the semantics. As an application, and its semantics have been implemented on top of the machine language, and are embedded in the Foundational Proof-Carrying Code project to produce memory-safety proofs for machine-language programs. [ABSTRACT FROM AUTHOR]