Automatic symbolic compositional verification by learning assumptions

Wonhong Nam, P. Madhusudan, Rajeev Alur

Research output: Contribution to journalArticlepeer-review


Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify appropriate assumptions for components. In this paper, we propose a fully automated approach to compositional reasoning that consists of automated decomposition using a hypergraph partitioning algorithm for balanced clustering of variables, and discovering assumptions using the L* algorithm for active learning of regular languages. We present a symbolic implementation of the learning algorithm, and incorporate it in the model checker NuSmv. In some cases, our experiments demonstrate significant savings in the computational requirements of symbolic model checking.

Original languageEnglish (US)
Pages (from-to)207-234
Number of pages28
JournalFormal Methods in System Design
Issue number3
StatePublished - Jun 2008


  • Assume-guarantee reasoning
  • Compositional verification
  • Formal verification
  • Hypergraph partitioning
  • Regular language learning
  • Symbolic model checking

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'Automatic symbolic compositional verification by learning assumptions'. Together they form a unique fingerprint.

Cite this