Self-composition by Symbolic Execution

Author Quoc-Sang Phan

Thumbnail PDF


  • Filesize: 0.57 MB
  • 8 pages

Document Identifiers

Author Details

Quoc-Sang Phan

Cite AsGet BibTex

Quoc-Sang Phan. Self-composition by Symbolic Execution. In 2013 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 35, pp. 95-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Self-composition is a logical formulation of non-interference, a high-level security property that guarantees the absence of illicit information leakages through executing programs. In order to capture program executions, self-composition has been expressed in Hoare or modal logic, and has been proved (or refuted) by using theorem provers. These approaches require considerable user interaction, and verification expertise. This paper presents an automated technique to prove self-composition. We reformulate the idea of self-composition into comparing pairs of symbolic paths of the same program; the symbolic paths are given by Symbolic Execution. The result of our analysis is a logical formula expressing self-composition in first-order theories, which can be solved by off-the-shelf Satisfiability Modulo Theories solvers.
  • Information Flow
  • Symbolic Execution
  • Satisfiability Modulo Theories


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads