Relational abstract interpretation of arrays in assembly code

DOI10.1007/s10703-022-00399-3zbMath1522.68144OpenAlexW4299462755MaRDI QIDQ6108433

Julien Forget, Jordy Ruiz, Clément Ballabriga

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

polyhedraabstract interpretationarray analysisassembly code

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Inferring complete initialization of arrays
• An array content static analysis based on non-contiguous partitions
• The octagon abstract domain
• Static analysis of binary code with memory indirections using polyhedra
• Refinement-Based CFG Reconstruction from Unstructured Programs
• Abstraction of Optional Numerical Values
• Fully Bounded Polyhedral Analysis of Integers with Wrapping
• A framework for numeric analysis of array operations
• Tools and Algorithms for the Construction and Analysis of Systems
• Compiler Construction
• A parametric segmentation functor for fully automatic and scalable array content analysis
• What Else Is Decidable about Integer Arrays?
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation

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