2026-08-16T08:53:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4774 2024-03-06T10:29:41Z ddc:004 open_access

Symbolic Execution as DPLL Modulo Theories Phan, Quoc-Sang Symbolic Execution Satisfiability Modulo Theories 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Quoc-Sang Phan 2014 Is Part Of OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICCSW.2014.58 urn:nbn:de:0030-drops-47746 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.58 eng https://creativecommons.org/licenses/by/3.0/legalcode