Relational abstract interpretation of arrays in assembly code

DOI10.1007/S10703-022-00399-3MaRDI QIDQ6108433zbMATH OpenOpenAlexFDO

Authors Clément Ballabriga, Julien Forget, Jordy Ruiz

Publication date 29 June 2023

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-022-00399-3

zbMATH Keywords

abstract interpretationarray analysisassembly codepolyhedra

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1953021
• Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation
• An array content static analysis based on non-contiguous partitions
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Static analysis of binary code with memory indirections using polyhedra

Cites work

• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Abstraction of Optional Numerical Values
• An array content static analysis based on non-contiguous partitions
• Compiler Construction
• Computer Aided Verification
• Fully Bounded Polyhedral Analysis of Integers with Wrapping
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• Inferring complete initialization of arrays
• Refinement-based CFG reconstruction from unstructured programs
• Static analysis of binary code with memory indirections using polyhedra
• The octagon abstract domain
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• What Else Is Decidable about Integer Arrays?

Cited in

(5)

• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Generic abstraction of dictionaries and arrays
• A framework for numeric analysis of array operations
• Programming Languages and Systems
• An array content static analysis based on non-contiguous partitions

This page was built for publication: Relational abstract interpretation of arrays in assembly code

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