Verification, Model Checking, and Abstract Interpretation

DOI10.1007/11609773MaRDI QIDQ5898628zbMATH OpenOpenAlexFDO

Authors Antoine Miné

Publication date 12 February 2007

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

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Symbolic computation and algebraic computation (68W30)

Recommendations

• Static Analysis of Numerical Algorithms
• Static analysis of finite precision computations
• Abstract fixpoint computations with numerical acceleration methods
• Automatic modular abstractions for template numerical constraints
• scientific article; zbMATH DE number 1738295

Cited in

(23)

• Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
• Inferring functional properties of matrix manipulating programs by abstract interpretation
• View-augmented abstractions
• A note on the inversion join for polyhedral analysis
• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• Generalizing the template polyhedral domain
• Static contract checking with abstract interpretation
• Static analysis of finite precision computations
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Automatic modular abstractions for template numerical constraints
• Polynomial Precise Interval Analysis Revisited
• scientific article; zbMATH DE number 1262450 (Why is no real title available?)
• Discovering invariants via simple component analysis
• Inferring sufficient conditions with backward polyhedral under-approximations
• Stratified static analysis based on variable dependencies
• A zonotopic framework for functional abstractions
• A generic framework to coarse-grain stochastic reaction networks by abstract interpretation
• Context-sensitive meta-constraint systems for explainable program analysis
• The two variable per inequality abstract domain
• Rigorous error analysis of numerical algorithms via symbolic computations
• Why does Astrée scale up?
• A minimalistic look at widening operators

Describes a project that uses

Uses Software

• ASTREE
• Octagon

This page was built for publication: Verification, Model Checking, and Abstract Interpretation

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