Symbolic compositional verification by learning assumptions

Rajeev Alur, P. Madhusudan, Wonhong Nam

Research output: Contribution to journalConference article

Abstract

The verification problem for a system consisting of components can be decomposed into simpler subproblems for the components using assume-guarantee reasoning. However, such compositional reasoning requires user guidance to identify appropriate assumptions for components. In this paper, we propose an automated solution for discovering assumptions based on 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. Our experiments demonstrate significant savings in the computational requirements of symbolic model checking.

Original languageEnglish (US)
Pages (from-to)548-562
Number of pages15
JournalLecture Notes in Computer Science
Volume3576
DOIs
StatePublished - 2005
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this