Symbolic execution as DPLL modulo theories

DOI10.4230/OASICS.ICCSW.2014.58MaRDI QIDQ5240106zbMATH OpenOpenAlexFDO

Authors Quoc-Sang Phan

Publication date 24 October 2019

Full work available at URL https://dblp.uni-trier.de/db/conf/iccsw/iccsw2014.html#Phan14

zbMATH Keywords

satisfiability modulo theoriessymbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Symbolic execution formally explained
• Symbolic execution: A semantic approach
• Demand-Driven Compositional Symbolic Execution
• An abstract interpretation of DPLL(T)
• Symbolic execution based on language transformation

Cites work

• A Decision Procedure for Bit-Vectors and Arrays
• A machine program for theorem-proving
• Lazy satisfiability modulo theories
• Symbolic execution and program testing
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

Cited in

(11)

• Symbolic execution: A semantic approach
• Symbolic execution formally explained
• Backward symbolic execution with loop folding
• Efficient loop navigation for symbolic execution
• Symbolic memory with pointers
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• scientific article; zbMATH DE number 1796151 (Why is no real title available?)
• Compact symbolic execution
• Demand-Driven Compositional Symbolic Execution
• Mixed concrete-symbolic predicate transformer
• On the nature of symbolic execution

Describes a project that uses

Uses Software

• z3
• MathSAT
• STP

This page was built for publication: Symbolic execution as DPLL modulo theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5240106)