Article contents
Automatically inferring loop invariants via algorithmic learning†
Published online by Cambridge University Press: 17 December 2014
Abstract
By combining algorithmic learning, decision procedures, predicate abstraction and simple templates for quantified formulae, we present an automated technique for finding loop invariants. Theoretically, this technique can find arbitrary first-order invariants (modulo a fixed set of atomic propositions and an underlying satisfiability modulo theories solver) in the form of the given template and exploit the flexibility in invariants by a simple randomized mechanism. In our study, the proposed technique was able to find quantified invariants for loops from the Linux source and other realistic programs. Our contribution is a simpler technique than the previous works yet with a reasonable derivation power.
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 25 , Issue 4: APLAS 2010 , May 2015 , pp. 892 - 915
- Copyright
- Copyright © Cambridge University Press 2014
Footnotes
This work was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology (MEST) / National Research Foundation of Korea (NRF) (Grant 2011-0000971), the National Science Foundation (award no. CNS0926181), the National Science Council of Taiwan projects No. NSC97-2221-E-001-003-MY3, NSC97-2221-E-001-006-MY3, the FORMES Project within LIAMA Consortium, and the French ANR project SIVES ANR-08-BLAN-0326-01. This research was sponsored in part by the National Science Foundation (award no. CNS0926181) and by Republic of Korea Dual Use Program Cooperation Center (DUPC) of Agency for Defense Development (ADD).
References
- 3
- Cited by