CfPBoK
by
Vadim Zaytsev
sle2014s/paper03
SLE 2014 SI
paper:
Symbolic execution based on language transformation
Andrei Arusoaie
,
Dorel Lucanu
,
Vlad Rusu
DOI:
10.1016/j.cl.2015.08.004
Extended version of
A Generic Framework for Symbolic Execution
(
SLE 2013
)
T4C: Vertical Transformation
Starting from a formal operational semantics, the paper automatically generates a transformed “symbolic” language definition enabling symbolic execution.
T1C: Behavioural Semantics
The technique is semantics-driven: it relies on executable operational semantics (term rewriting) as the basis for execution/analysis.
T5D: Formal Methods
Symbolic execution, reachability analysis, and model checking are core formal-methods goals and evaluation targets.
T4A: Workbenches
A prototype is implemented inside the K framework’s compilation pipeline, i.e., as language-engineering tooling.
The page is maintained by
Dr. Vadim Zaytsev
a.k.a. @
grammarware
. Last updated: June 2026.