Advertisement
Published in:
2010 | OriginalPaper | Chapter
Merit: An Interpolating Model-Checker
Author : Nicolas Caniart
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We present the tool
Merit
, a
Cegar
model-checker for safety properties of counter-systems, which sits in the Lazy Abstraction with Interpolants (
lawi
) framework.
lawi
is parametric with respect to the interpolation technique and so is
Merit
. Thanks to its open architecture,
Merit
makes it possible to experiment new refinement techniques without having to re-implement the generic, technical part of the framework. In this paper, we first recall the basics of the
lawi
algorithm. We then explain two heuristics in order to help termination of the
Cegar
loop: the first one presents different approaches to symbolically compute interpolants. The second one focuses on how to improve the unwinding strategy. We finally report our experimental results, obtained using those heuristics, on a large amount of classical models.