SAT-Based Compositional Verification Using Lazy Learning

Abstract. A recent approach to automated assume-guarantee reasoning (AGR) for concurrent systems relies on computing environment assumptions for components using the L algorithm for learning regular languages. While this approach has been investigated extensively for message passing systems, it still remains a challenge to scale the technique to large shared memory systems, mainly because the assumptions have an exponential communication alphabet size. In this paper, we propose a SAT-based methodology that employs both induction and interpolation to implement automated AGR for shared memory systems. The method is based on a new lazy approach to assumption learning, which avoids an explicit enumeration of the exponential alphabet set during learning by using symbolic alphabet clustering and iterative counterexample-driven localized partitioning. Preliminary experimental results on benchmarks in Verilog and SMV are encouraging and show that the approach scales well in practice.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Nishant Sinha, Edmund M. Clarke
• Keywords: CAV 2007, Exponential Communication Alphabet, Hardware, Large Shared Memory, Shared Memory Systems