Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning

Yu-Fang Chen 1 Edmund Clarke 2 Azadeh Farzan 3 Fei He 4, 5 Ming-Hsien Tsai 6 Yih-Kuen Tsay 6 Bow-Yaw Wang 4, 5, 1 Lei Zhu 5
1 Academia Sinica
2 Computer Science Department - Carnegie Mellon University
3 University of Toronto
4 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
5 Tsinghua University [Beijing]
6 NTU - National Taiwan University [Taiwan]
Abstract : We compare two learning algorithms for generating contextual assumptions in automated assume-guarantee reasoning. The CDNF algorithm implicitly represents contextual assumptions by a conjunction of DNF formulae, while the OBDD learning algorithm uses ordered binary decision diagrams as its representation. Using these learning algorithms, the performance of assume-guarantee reasoning is compared with monolithic interpolation-based Model Checking in parametrized hardware test cases.
Keywords : assume-guarantee reasoning learning model checking formal verification
Type de document :
Communication dans un congrès
Bernhard Steffen. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2010, Crete, Greece. 2010, LNCS
Liste complète des métadonnées
https://hal.inria.fr/inria-00515167
Contributeur : Bow-Yaw Wang <>
Soumis le : lundi 6 septembre 2010 - 03:50:07
Dernière modification le : mercredi 10 octobre 2018 - 14:28:10

Identifiants

  • HAL Id : inria-00515167, version 1

Collections

INRIA | LIAMA | CIRAD | INRA | INRIA-ROCQ

Citation

Yu-Fang Chen, Edmund Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, et al.. Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. Bernhard Steffen. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2010, Crete, Greece. 2010, LNCS. 〈inria-00515167〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

290

Contact


archive-ouverte@inria.fr