A compositional logic for control flow

Gang Tan, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings
Pages80-94
Number of pages15
StatePublished - Jul 6 2006
Event7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006 - Charleston, SC, United States
Duration: Jan 8 2006Jan 10 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3855 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006
CountryUnited States
CityCharleston, SC
Period1/8/061/10/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A compositional logic for control flow'. Together they form a unique fingerprint.

  • Cite this

    Tan, G., & Appel, A. W. (2006). A compositional logic for control flow. In Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings (pp. 80-94). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3855 LNCS).