A scalable segmented decision tree abstract domain

DOI10.1007/978-3-642-13754-9_5MaRDI QIDQ3587252zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Publication date 7 September 2010

Published in Time for Verification (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00543632/file/segmentation.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• Why does Astrée scale up?
• Fast polyhedra abstract domain
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Static Analysis

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Abstract interpretation and application to logic programs
• Abstract Interpretation Frameworks
• Abstract interpretation using typed decision graphs
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 3485178 (Why is no real title available?)
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• scientific article; zbMATH DE number 1487852 (Why is no real title available?)
• Programming Languages and Systems
• Static analysis of arithmetical congruences
• Systematic design of program transformation frameworks by abstract interpretation
• The octagon abstract domain
• Verification by abstract interpretation

Cited in

(12)

• A decision tree lifted domain for analyzing program families with numerical features
• Finding suitable variability abstractions for lifted analysis
• Range and set abstraction using SAT
• Quadtrees as an abstract domain
• Partitioned memory models for program analysis
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• Access-based localization for octagons
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• A parametric segmentation functor for fully automatic and scalable array content analysis
• String abstract domains and their combination
• Quantitative program sketching using lifted static analysis
• Why does Astrée scale up?

Describes a project that uses

Uses Software

• ASTREE

This page was built for publication: A scalable segmented decision tree abstract domain

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