A generic framework for symbolic execution: a coinductive approach

DOI10.1016/j.jsc.2016.07.012zbMath1356.68044OpenAlexW1439634531MaRDI QIDQ507361

Dorel Lucanu, Andrei Arusoaie, Vlad Rusu

Publication date: 6 February 2017

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01238696/file/JSC-PAS_2013_submission_10.pdf

zbMATH Keywords

programming languageprogram verificationsymbolic executioncircular coinductionformal operational semanticsreachability logic

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (10)

Executing and verifying higher-order functional-imperative programs in Maude ⋮ A matching logic foundation for Alk ⋮ Program equivalence by circular reasoning ⋮ Symbolic execution formally explained ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ A language-independent proof system for full program equivalence ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Proving Reachability-Logic Formulas Incrementally

Uses Software

• Coq
• CUTE
• Why3
• Spec#
• z3
• KLEE
• CIRC
• Maude
• DART
• Pex
• VeriFast
• TRACER
• WhyML
• K Prover
• STP

Cites Work

• Unnamed Item
• Unnamed Item
• A generic framework for symbolic execution: a coinductive approach
• Language definitions as rewrite theories
• 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
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• Circular Coinduction: A Proof Theoretical Foundation
• TRACER: A Symbolic Execution Tool for Verification
• Rewriting Modulo SMT and Open System Analysis
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Introduction to Bisimulation and Coinduction
• On the Foundations of Corecursion
• Symbolic execution and program testing
• Fast Pattern Matching in Strings
• From Hoare Logic to Matching Logic Reachability
• All-Path Reachability Logic
• Variant Narrowing and Equational Unification
• One-Path Reachability Logic
• Matching Logic - Extended Abstract (Invited Talk)
• Model Checking Software
• Why3 — Where Programs Meet Provers
• Programming Languages and Systems

This page was built for publication: A generic framework for symbolic execution: a coinductive approach