Skip to Main content Skip to Navigation
Conference papers

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

yungbum Jung 1 Soonho Kong 1 Bow-yaw Wang 2 Kwangkeun yi 1 
2 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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00517257
Contributor : Bow-Yaw Wang Connect in order to contact the contributor
Submitted on : Tuesday, September 14, 2010 - 3:10:36 AM
Last modification on : Thursday, February 3, 2022 - 11:16:52 AM

Identifiers

  • 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. ⟨inria-00517257⟩

Share

Metrics

Record views

110