Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths

DOI10.1007/978-3-319-43144-4_3zbMATH Open1478.68140OpenAlexW2494909361MaRDI QIDQ2829242FDOQ2829242

Authors: Romain Aissat, Frédéric Voisin, Burkhart Wolff 

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_3

Recommendations

• TRACER: a symbolic execution tool for verification
• scientific article; zbMATH DE number 1982210
• Symbolic trajectory evaluation
• Dynamic Path Reduction for Software Model Checking
• Compact symbolic execution

zbMATH Keywords

graph transformationsymbolic executionfeasible pathsCEGARcontrol-flow graphsTRACER

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Locales: a module system for mathematical theories
• Lazy Abstraction with Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• TRACER: a symbolic execution tool for verification
• A graph library for Isabelle

Cited In (3)

• TRACER: a symbolic execution tool for verification
• A theory for control-flow graph exploration
• SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement

Uses Software

• BLAST
• CEGAR
• TRACER
• Locales
• SatAbs
• Graph Theory

This page was built for publication: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths

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