M.Sc Thesis | |
M.Sc Student | Abdelkader Karam |
---|---|
Subject | Automated Circular Assume-Guarantee Reasoning |
Department | Department of Computer Science | Supervisors | ASSOCIATE PROFESSOR Sharon Shoham-Buchbind |
PROFESSOR EMERITUS Orna Grumberg | |
Full Thesis text | ![]() |
Model
checking is a successful approach for verifying hardware and software systems.
Despite its success, the technique suffers from the state explosion problem
which arises due to the huge state space of real-life systems. The size of the
model induces high memory and time requirements that may make model checking
not applicable to large systems.
One solution to face the state explosion problem is the use of compositional
verification, that aims to decompose the verification of a large system into
the more manageable verification of its components. To account for dependencies
between the components, assume-guarantee reasoning defines rules that break-up
the global verification of a system into local verification of individual
components, using assumptions about the rest of the program.
In recent years, compositional techniques have gained significant successes
following a breakthrough in the ability to automate assume-guarantee reasoning.
However, automation is still restricted to simple acyclic assume-guarantee
rules.
In this work, we focus on automating circular
assume-guarantee reasoning in which the verification of individual
components mutually depends on each other. We use a sound and complete circular
assume-guarantee rule and we describe how to automatically build the
assumptions needed for using the rule. Our algorithm accumulates joint constraints on the
assumptions based on (spurious) counterexamples obtained from checking the
premises of the rule, and uses
a SAT solver to synthesize minimal assumptions that satisfy these constraints.
To the best of our knowledge, our work is the first to fully automate circular
assume-guarantee reasoning.
We implemented our approach and compared it with an established learning-based
method that uses an acyclic rule. In all cases, the assumptions generated for
the circular rule were significantly smaller, leading to smaller verification
problems. Further, on larger examples, we obtained a significant speedup as
well.