TY - GEN
T1 - A compositional logic for control flow
AU - Tan, Gang
AU - Appel, Andrew W.
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33745652704&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745652704&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:33745652704
SN - 3540311394
SN - 9783540311393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 80
EP - 94
BT - Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings
T2 - 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006
Y2 - 8 January 2006 through 10 January 2006
ER -