Automated Assume-Guarantee Reasoning through Implicit Learning

Yu-Fang Chen 1 Edmund Clarke 2 Azadeh Farzan 3 Ming-Hsien Tsai 4 Yih-Kuen Tsay 4 Bow-Yaw Wang 5, 1, *
* Auteur correspondant
5 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 : mercredi 10 octobre 2018 - 14:28:10

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

230