Symbolic execution based on language transformation

DOI10.1016/j.cl.2015.08.004zbMath1387.68047OpenAlexW2291243181MaRDI QIDQ1749128

Dorel Lucanu, Andrei Arusoaie, Vlad Rusu

Publication date: 15 May 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01186008/file/clss2015.pdf

zbMATH Keywords

formal semanticsprogramming languagesprogram analysissymbolic execution

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items (3)

Executing and verifying higher-order functional-imperative programs in Maude ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

Uses Software

• CUTE
• z3
• Maude
• DART
• Pex
• K tool
• K-Java
• KLOVERA
• K Prover
• KOOL
• STP

Cites Work

• Unnamed Item
• Foundations of algebraic specification and formal software development.
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• An overview of the K semantic framework
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A rewriting logic approach to operational semantics
• Symbolic execution and program testing
• From Hoare Logic to Matching Logic Reachability
• Variant Narrowing and Equational Unification
• Model Checking Software
• Programming Languages and Systems

This page was built for publication: Symbolic execution based on language transformation