DROPS

Document

DOI: 10.4230/OASIcs.ICCSW.2014.58

Symbolic Execution as DPLL Modulo Theories

Authors: Quoc-Sang Phan

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

We show how Symbolic Execution can be understood as a variant of the DPLL(T ) algorithm, which is the dominant technique for the Satisfiability Modulo Theories (SMT) problem. In other words, Symbolic Executors are SMT solvers. This view enables us to use an SMT solver, with the ability of generating all models with respect to a set of Boolean atoms, to explore all symbolic paths of a program. This results in a more lightweight approach for Symbolic Execution.

Cite as

Quoc-Sang Phan. Symbolic Execution as DPLL Modulo Theories. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 58-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{phan:OASIcs.ICCSW.2014.58,
  author =	{Phan, Quoc-Sang},
  title =	{{Symbolic Execution as DPLL Modulo Theories}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{58--65},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.58},
  URN =		{urn:nbn:de:0030-drops-47746},
  doi =		{10.4230/OASIcs.ICCSW.2014.58},
  annote =	{Keywords: Symbolic Execution, Satisfiability Modulo Theories}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2013.95

Self-composition by Symbolic Execution

Authors: Quoc-Sang Phan

Published in: OASIcs, Volume 35, 2013 Imperial College Computing Student Workshop

Abstract

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{phan:OASIcs.ICCSW.2013.95,
  author =	{Phan, Quoc-Sang},
  title =	{{Self-composition by Symbolic Execution}},
  booktitle =	{2013 Imperial College Computing Student Workshop},
  pages =	{95--102},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-63-7},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{35},
  editor =	{Jones, Andrew V. and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2013.95},
  URN =		{urn:nbn:de:0030-drops-42770},
  doi =		{10.4230/OASIcs.ICCSW.2013.95},
  annote =	{Keywords: Information Flow, Symbolic Execution, Satisfiability Modulo Theories}
}

Search Results

Documents authored by Phan, Quoc-Sang

Symbolic Execution as DPLL Modulo Theories

Abstract

Cite as

Self-composition by Symbolic Execution

Abstract

Cite as

Thanks for your feedback!

Could not send message