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

DOI10.1007/978-3-319-43144-4_3MaRDI QIDQ2829242zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

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

Describes a project that uses

Uses Software

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

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)