Abstract Interpretation of Symbolic Execution with Explicit State Updates

DOI10.1007/978-3-642-04167-9_13MaRDI QIDQ3638994zbMATH OpenOpenAlexFDO

Authors Richard Bubel, Reiner Hähnle, Benjamin Weiß

Publication date 28 October 2009

Published in Formal Methods for Components and Objects (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-04167-9_13

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Abstract Interpretation as Automated Deduction
• scientific article; zbMATH DE number 2064465
• Abstract interpretation
• scientific article; zbMATH DE number 1953018
• scientific article; zbMATH DE number 2087617

Cites work

• A semantic approach to secure information flow
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• Integration of a security type system into a program logic
• Non-termination Checking for Imperative Programs
• On flow-sensitive security types
• Predicate Abstraction in a Program Logic Calculus
• Programming Languages and Systems
• Programming Languages and Systems
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Static Analysis

Cited in

(8)

• Interleaving symbolic execution and partial evaluation
• Information flow in object-oriented software
• scientific article; zbMATH DE number 2064465 (Why is no real title available?)
• Verification conditions for source-level imperative programs
• Symbolic abstract heaps for polymorphic information-flow guard inference
• A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3
• Sound symbolic execution via abstract interpretation and its application to security
• Abstract execution

Describes a project that uses

Uses Software

• KRAKATOA
• SPIN
• Why3
• Spec#
• Caduceus
• KIV
• ASTREE

This page was built for publication: Abstract Interpretation of Symbolic Execution with Explicit State Updates

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