Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
VMCAI'10: Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation(2010)
摘要
By combining algorithmic learning, decision procedures, and predicate abstraction, we present an automated technique for finding loop invariants in propositional formulae. Given invariant approximations derived from pre- and post-conditions, our new technique exploits the flexibility in invariants by a simple randomized mechanism. The proposed technique is able to generate invariants for some Linux device drivers and SPEC2000 benchmarks in our experiments.
更多查看译文
关键词
predicate abstraction,decision procedure,proposed technique,invariant approximation,deriving invariants,loop invariants,automated technique,spec2000 benchmarks,linux device driver,algorithmic learning,new technique
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要