Automated AssumeGuarantee Reasoning through Implicit Learning, in "Computer Aided Verification

Abstract. We propose a purely implicit solution to the contextual as-sumption 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 assump-tions by the CDNF algorithm — a learning algorithm for Boolean func-tions. We report three parametrized test cases where our solution out-performs the monolithic interpolation-based Model Checking algorithm.