Sciweavers

Share
FMSD
2008

Automatic symbolic compositional verification by learning assumptions

10 years 10 months ago
Automatic symbolic compositional verification by learning assumptions
Abstract 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. Keywords Formal verification
Wonhong Nam, P. Madhusudan, Rajeev Alur
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FMSD
Authors Wonhong Nam, P. Madhusudan, Rajeev Alur
Comments (0)
books