SMT-AI: an Abstract Interpreter as Oracle for k-induction

详细信息    查看全文

• 作者：Pierre Roux ; Ré ; mi Delmas ; Pierre-Loï ; c Garoche
• 关键词：k-induction ; abstract interpretation ; lemmas generator ; SMT
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2010
• 出版时间：October 2010
• 年：2010
• 卷：267
• 期：2
• 页码：55-68
• 全文大小：452 K

文摘

The last decade has seen a major development of verification techniques based on SMT solvers used to prove inductive invariants on systems. This approach allows to prove functional properties and scale up to handle industrial problems. However, it often needs a man in the loop to provide hand-written lemmas on the system in order to help the analysis and complete the proof.

This paper presents a tool that automatically generates lemmas. It takes such systems and over-approximates their collecting semantics, providing a bound on the numerical memories. It is based on the abstract interpretation methodology introduced by Cousot in 1977.