Automated Assume-Guarantee Reasoning through Implicit Learning

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: Conference
• Year: 2010
• Where: CAV
• Authors: Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang
• Keywords: Algorithm, CAV 2010, Contextual Assumptions, Hardware, Learning Algorithm