Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction

Yungbum Jung Soonho Kong Bow-Yaw Wang 1 Kwangkeun Yi
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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.
Type de document :
Communication dans un congrès
Verification, Model Checking, and Abstract Interpretation, Jan 2010, Madrid, Spain. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00517257
Contributeur : Bow-Yaw Wang <>
Soumis le : mardi 14 septembre 2010 - 03:10:36
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29

Identifiants

  • HAL Id : inria-00517257, version 1

Collections

Citation

Yungbum Jung, Soonho Kong, Bow-Yaw Wang, Kwangkeun Yi. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. Verification, Model Checking, and Abstract Interpretation, Jan 2010, Madrid, Spain. 2010. 〈inria-00517257〉

Partager

Métriques

Consultations de la notice

147