Infeasible Paths Elimination by Symbolic Execution Techniques

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

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

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)

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

Uses Software

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

This page was built for publication: Infeasible Paths Elimination by Symbolic Execution Techniques

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