Skip to Main content Skip to Navigation
Conference papers

Automated Assume-Guarantee Reasoning through Implicit Learning

yu-Fang Chen 1 Edmund M. Clarke 2 Azadeh Farzan 3 Ming-Hsien Tsai 4 yih-Kuen Tsay 4 Bow-yaw Wang 5, 1, * 
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Bow-Yaw Wang Connect in order to contact the contributor
Submitted on : Friday, July 2, 2010 - 8:12:20 AM
Last modification on : Tuesday, May 3, 2022 - 3:14:04 PM


  • HAL Id : inria-00496949, version 1



yu-Fang Chen, Edmund M. 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. ⟨inria-00496949⟩



Record views