Infeasible Paths Elimination by Symbolic Execution Techniques

DOI10.1007/978-3-319-43144-4_3zbMath1478.68140OpenAlexW2494909361MaRDI QIDQ2829242

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

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

Uses Software

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

Cites Work

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

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