Inferring functional properties of matrix manipulating programs by abstract interpretation

DOI10.1007/s10703-017-0311-xzbMath1425.68074OpenAlexW2794307297MaRDI QIDQ1791274

Matthieu Journault, Antoine Miné

Publication date: 4 October 2018

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

Full work available at URL: https://doi.org/10.1007/s10703-017-0311-x

zbMATH Keywords

static analysisabstract interpretationfunctional correctnessmatrix manipulating programs

Mathematics Subject Classification ID

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

Uses Software

• FLAME
• ASTREE
• FunArray

Cites Work

• Unnamed Item
• Unnamed Item
• The octagon abstract domain
• Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
• Verification: Theory and practice. Essays dedicated to Zohar Manna on the occasion of his 64th birthday.
• Fluid Updates: Beyond Strong vs. Weak Updates
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Invariant and Type Inference for Matrices
• Abstract cofibered domains: Application to the alias analysis of untyped programs
• A framework for numeric analysis of array operations
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal certification of a compiler back-end or
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• FLAME
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Inferring functional properties of matrix manipulating programs by abstract interpretation