Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates

Résumé

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.
Fichier non déposé

Dates et versions

inria-00515166 , version 1 (06-09-2010)

Identifiants

  • HAL Id : inria-00515166 , version 1

Citer

Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, Kwangkeun Yi. Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. ASIAN Symposium on Programming Languages and Systems, Nov 2010, Shanghai, China. ⟨inria-00515166⟩
134 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More