License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2014.58
URN: urn:nbn:de:0030-drops-47746
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4774/
Go to the corresponding OASIcs Volume Portal

Phan, Quoc-Sang

Symbolic Execution as DPLL Modulo Theories

pdf-format:
11.pdf (0.6 MB)

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.

BibTeX - Entry

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

Keywords: Symbolic Execution, Satisfiability Modulo Theories
Collection: 2014 Imperial College Computing Student Workshop
Issue Date: 2014
Date of publication: 08.10.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI