We present a program logic, ℒ c, which modularly reasons about unstructured control flow in machine-language programs. Unlike previous program logics, the basic reasoning units in ℒ c are multiple-entry and multiple-exit program fragments, ℒ c 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 ℒ c and prove that the logic is both sound and complete with respect to the semantics. As an application, ℒ c and its semantics have been implemented on top of the SPARC machine language, and are embedded in the Foundational Proof-Carrying Code project to produce memory-safety proofs for machine-language programs. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Tan, G., & Appel, A. W. (2006). A compositional logic for control flow. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3855 LNCS, pp. 80–94). https://doi.org/10.1007/11609773_6
Mendeley helps you to discover research relevant for your work.