Lifting numeric relational domains to algebraic data types

DOI10.1007/978-3-031-22308-2_6MaRDI QIDQ6164423zbMATH OpenOpenAlexFDO

Authors

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-22308-2_6

zbMATH Keywords

abstract interpretationalgebraic data typesfunction summariesinput-output relationsrelational abstract domainsstatic analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 1948392
• A relational shape abstract domain
• An abstract domain of uninterpreted functions
• An abstract domain for trees with numeric relations

Cites work

• A completion algorithm for lattice tree automata
• A new abstraction framework for affine transformers
• A relational shape abstract domain
• Abstract cofibered domains: application to the alias analysis of untyped programs
• Abstraction of Optional Numerical Values
• An abstract domain for trees with numeric relations
• Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
• Disjunctive relational abstract interpretation for interprocedural program analysis
• Grammar Analysis and Parsing by Abstract Interpretation
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• scientific article; zbMATH DE number 1231565 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 2087567 (Why is no real title available?)
• scientific article; zbMATH DE number 7361354 (Why is no real title available?)
• scientific article; zbMATH DE number 2238212 (Why is no real title available?)
• Interprocedural shape analysis using separation logic-based transformer summaries
• Precise interprocedural analysis in the presence of pointers to the stack
• Principles of abstract interpretation
• Programming Languages and Systems
• Semantic-directed clumping of disjunctive abstract states
• Static Analysis
• The octagon abstract domain
• Types and programing languages
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Verifying higher-order functions with tree automata
• Why3 -- where programs meet provers

Cited in

(3)

• An input-output relational domain for algebraic data types and functional arrays
• Preface of the special issue on the static analysis symposium 2020 and 2022
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness

This page was built for publication: Lifting numeric relational domains to algebraic data types

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