Skip to Main content Skip to Navigation
Conference papers

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 THU - 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
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00515167
Contributor : Bow-Yaw Wang <>
Submitted on : Monday, September 6, 2010 - 3:50:07 AM
Last modification on : Tuesday, June 1, 2021 - 2:34:10 PM

Identifiers

  • HAL Id : inria-00515167, version 1

Collections

INRIA | LIAMA | CIRAD | CNRS | INRA | INRAE

Citation

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

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

381

 

Contact                    Legal Notice                    Personal Data