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.