Why does Astrée scale up?

DOI10.1007/S10703-009-0089-6MaRDI QIDQ845249zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot, Laurent Mauborgne, Antoine Miné, Xavier Rival, 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 methodsScalabilitySafetyAbstract InterpretationEmbedded critical softwareStatic analysis tool\texttt{Astrée}

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis
• A scalable segmented decision tree abstract domain
• Programming Languages and Systems

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 3792232 (Why is no real title available?)
• scientific article; zbMATH DE number 3592938 (Why is no real title available?)
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 1759702 (Why is no real title available?)
• scientific article; zbMATH DE number 2087547 (Why is no real title available?)
• scientific article; zbMATH DE number 2087567 (Why is no real title available?)
• scientific article; zbMATH DE number 1832227 (Why is no real title available?)
• scientific article; zbMATH DE number 1390341 (Why is no real title available?)
• A class of polynomially solvable range constraints for interval analysis without widenings
• Abstract interpretation and application to logic programs
• An axiomatic basis for computer programming
• Automatically Refining Abstract Interpretations
• Constructive versions of Tarski's fixed point theorems
• Fixpoint-Guided Abstraction Refinements
• Graph-Based Algorithms for Boolean Function Manipulation
• Making abstract interpretations complete
• Optimal domains for disjunctive abstract interpretation
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis
• Static analysis of arithmetical congruences
• The octagon abstract domain
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

Cited in

(20)

• Abstract interpretation of microcontroller code: intervals meet congruences
• Programming Languages and Systems
• A sparse evaluation technique for detailed semantic analyses
• Block-wise abstract interpretation by combining abstract domains with SMT
• A tree-based approach to data flow proofs
• Incremental and modular context-sensitive analysis
• Precise interprocedural analysis in the presence of pointers to the stack
• Sparsity preserving algorithms for octagons
• A scalable segmented decision tree abstract domain
• Range and set abstraction using SAT
• ASTREE
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• Quadtrees as an abstract domain
• Programming Languages and Systems
• Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
• Clustered relational thread-modular abstract interpretation with local traces
• Abstract semantic dependency
• On the Monniaux problem in abstract interpretation
• Three improvements to the top-down solver
• Static Analysis

Describes a project that uses

Uses Software

• CBMC
• OCaml
• Dagger
• Apron

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

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