Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates

Soonho Kong 1 Yungbum Jung 1 Cristina David 2 Bow-Yaw Wang 3, 4 Kwangkeun Yi 1
1 Seoul National University [Seoul]
2 NUS - National University of Singapore
3 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
4 Academia Sinica
Abstract : By combining algorithmic learning, decision procedures, predicate abstraction, and simple templates, we present an automated technique for finding quantified loop invariants. Our technique can find arbitrary first-order invariants (modulo a fixed set of atomic propositions and an underlying SMT solver) in the form of the given template and exploits the flexibility in invariants by a simple randomized mechanism. The proposed technique is able to find quantified invariants for loops from the Linux source, as well as for the benchmark code used in the previous works. Our contribution is a simpler technique than the previous works yet with a reasonable derivation power.
Keywords : loop invariants learning program verification
Type de document :
Communication dans un congrès
Kazunori Ueda. ASIAN Symposium on Programming Languages and Systems, Nov 2010, Shanghai, China. 2010, LNCS
Liste complète des métadonnées
https://hal.inria.fr/inria-00515166
Contributeur : Bow-Yaw Wang <>
Soumis le : lundi 6 septembre 2010 - 03:37:05
Dernière modification le : mercredi 10 octobre 2018 - 14:28:10

Identifiants

  • HAL Id : inria-00515166, version 1

Collections

INRIA | LIAMA | CIRAD | INRA | INRIA-ROCQ

Citation

Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi. Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. Kazunori Ueda. ASIAN Symposium on Programming Languages and Systems, Nov 2010, Shanghai, China. 2010, LNCS. 〈inria-00515166〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

345

Contact


archive-ouverte@inria.fr