Trace partitioning in abstract interpretation based static analyzers

DOI10.1007/978-3-540-31987-0_2MaRDI QIDQ5316570zbMATH OpenOpenAlexFDO

Authors Laurent Mauborgne, Xavier Rival

Publication date 13 September 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107380

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• An automata-based approach to trace partitioned abstract interpretation
• The ASTREÉ analyzer
• A combination framework for tracking partition sizes
• Refinement of Trace Abstraction
• Modular static program analysis

Cited in

(29)

• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Static analysis of embedded real-time concurrent software with dynamic priorities
• Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
• A framework for memory efficient context-sensitive program analysis
• Static analysis of ReLU neural networks with tropical polyhedra
• Certified compilation for cryptography: extended x86 instructions and constant-time verification
• Twinning automata and regular expressions for string static analysis
• A sparse evaluation technique for detailed semantic analyses
• Refinement of worst-case execution time bounds by graph pruning
• An automata-based approach to trace partitioned abstract interpretation
• A note on the inversion join for polyhedral analysis
• Automatic inference of access permissions
• Sound non-statistical clustering of static analysis alarms
• Partitioned memory models for program analysis
• Refinement-based CFG reconstruction from unstructured programs
• String analysis as an abstract interpretation
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Splitting the Control Flow with Boolean Flags
• Watchpoint semantics: A tool for compositional and focussed static analyses
• Sweeping in Abstract Interpretation
• Convex invariant refinement by control node splitting: a heuristic approach
• A combination framework for tracking partition sizes
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Programming Languages and Systems
• Clustered relational thread-modular abstract interpretation with local traces
• Verifying numerical programs via iterative abstract testing
• Why does Astrée scale up?
• The octagon abstract domain

Describes a project that uses

Uses Software

• ASTREE
• Octagon

This page was built for publication: Trace partitioning in abstract interpretation based static analyzers

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