Automated Assume-Guarantee Reasoning through Implicit Learning

Yu-Fang Chen Edmund Clarke Azadeh Farzan Ming-Hsien Tsai Yih-Kuen Tsay Bow-Yaw Wang 1, *
* Auteur correspondant
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 : We propose a purely implicit solution to the contextual assumption generation problem in assume-guarantee reasoning. Instead of improving the L* algorithm — a learning algorithm for finite automata, our algorithm computes implicit representations of contextual assumptions by the CDNF algorithm — a learning algorithm for Boolean functions. We report three parametrized test cases where our solution outperforms the monolithic interpolation-based Model Checking algorithm.
Type de document :
Communication dans un congrès
Computer Aided Verification, 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00496949
Contributeur : Bow-Yaw Wang <>
Soumis le : vendredi 2 juillet 2010 - 08:12:20
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29

Identifiants

  • HAL Id : inria-00496949, version 1

Collections

Citation

Yu-Fang Chen, Edmund Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, et al.. Automated Assume-Guarantee Reasoning through Implicit Learning. Computer Aided Verification, 2010, Edinburgh, United Kingdom. 2010. 〈inria-00496949〉

Partager

Métriques

Consultations de la notice

177