Why does Astrée scale up?

DOI10.1007/s10703-009-0089-6zbMath1185.68241OpenAlexW2165086189MaRDI QIDQ845249

Xavier Rival, Antoine Miné, Patrick Cousot, Laurent Mauborgne, Radhia Cousot, Jerome Feret

Publication date: 5 February 2010

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

Full work available at URL: https://doi.org/10.1007/s10703-009-0089-6

zbMATH Keywords

VerificationFormal methodsScalabilitySafety\texttt{Astrée}Abstract InterpretationEmbedded critical softwareStatic analysis tool

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (14)

A tree-based approach to data flow proofs ⋮ Learning a Strategy for Choosing Widening Thresholds from a Large Codebase ⋮ Sparsity preserving algorithms for octagons ⋮ Three improvements to the top-down solver ⋮ Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Precise Interprocedural Analysis in the Presence of Pointers to the Stack ⋮ TreeKs: A Functor to Make Numerical Abstract Domains Scalable ⋮ Enforcing termination of interprocedural analysis ⋮ Incremental and Modular Context-sensitive Analysis ⋮ Range and Set Abstraction using SAT ⋮ Quadtrees as an Abstract Domain ⋮ ASTREE ⋮ A sparse evaluation technique for detailed semantic analyses

Uses Software

• Apron
• Dagger
• OCaml
• CBMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• The octagon abstract domain
• Constructive versions of Tarski's fixed point theorems
• Optimal domains for disjunctive abstract interpretation
• A class of polynomially solvable range constraints for interval analysis without widenings
• Fixpoint-Guided Abstraction Refinements
• Graph-Based Algorithms for Boolean Function Manipulation
• Abstract interpretation and application to logic programs
• Static analysis of arithmetical congruences
• Tools and Algorithms for the Construction and Analysis of Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Making abstract interpretations complete
• Automatically Refining Abstract Interpretations
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Why does Astrée scale up?