Discovering invariants via simple component analysis

DOI10.1016/J.JSC.2011.12.052MaRDI QIDQ435979zbMATH OpenOpenAlexFDO

Authors Maurizio Parton, Francesca Scozzari, Gianluca Amato

Publication date 13 July 2012

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2011.12.052

zbMATH Keywords

algorithmsnumerical examplesabstract interpretationinterval arithmeticstatic analysissimple component analysis

Mathematics Subject Classification ID

Factor analysis and principal components; correspondence analysis (62H25) General methods in interval analysis (65G40)

Recommendations

• Deriving numerical abstract domains via principal component analysis
• Polynomial invariants by linear algebra
• Computer Aided Verification
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Algorithm to find invariant linear inequality constraints in programs

Cites work

• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 3829076 (Why is no real title available?)
• scientific article; zbMATH DE number 1956649 (Why is no real title available?)
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• scientific article; zbMATH DE number 1832225 (Why is no real title available?)
• scientific article; zbMATH DE number 1390341 (Why is no real title available?)
• scientific article; zbMATH DE number 7374771 (Why is no real title available?)
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Abstract interpretation and application to logic programs
• Affine relationships among variables of a program
• Deriving numerical abstract domains via principal component analysis
• Discovering affine equalities using random interpretation
• Interval arithmetic: from principles to implementation
• Inverse interval matrix: a survey
• Orthogonal simple component analysis: a new, exploratory approach
• Precise interprocedural analysis using random interpretation
• Program Analysis Using Symbolic Ranges
• Programming Languages and Systems
• Programming Languages and Systems
• Relational abstract domain of weighted hexagons
• Relational inductive shape analysis
• Simple Component Analysis
• Static analysis of arithmetical congruences
• The octagon abstract domain
• Two variables per linear inequality as an abstract domain
• Verification, Model Checking, and Abstract Interpretation
• 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

(9)

• Deriving numerical abstract domains via principal component analysis
• Unsupervised discovery of invariances
• The Daikon system for dynamic detection of likely invariants
• From invariant checking to invariant inference using randomized search
• The abstract domain of parallelotopes
• Experimental evaluation of numerical domains for inferring ranges
• Optimal multibinding unification for sharing and linearity analysis
• Descending chains and narrowing on template abstract domains
• Finding relevant templates via the principal component analysis

Describes a project that uses

Uses Software

• Apron
• R
• PPL
• DART
• Pex
• Lackwit
• Interproc
• InvGen
• ASTREE
• STP

This page was built for publication: Discovering invariants via simple component analysis

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