Discovering invariants via simple component analysis

详细信息    查看全文

• 作者：Gianluca Amato ^{amato@sci.unich.it} ; Maurizio Parton ^{parton@sci.unich.it} ; Francesca Scozzari ^{scozzari@sci.unich.it}
• 关键词：Static analysis ; Abstract interpretation ; Simple component analysis ; Intervals ; Interval arithmetic
• 刊名：Journal of Symbolic Computation
• 出版年：2012
• 出版时间：December, 2012
• 年：2012
• 卷：47
• 期：12
• 页码：1533-1560
• 全文大小：635 K

文摘

We propose a new technique combining dynamic and static analysis of programs to find linear invariants. We use a statistical tool, called simple component analysis, to analyze partial execution traces of a given program. We get a new coordinate system in the vector space of program variables, which is used to specialize numerical abstract domains. As an application, we instantiate our technique to interval analysis of simple imperative programs and show some experimental evaluations.