Merit: An Interpolating Model-Checker

9 years 7 months ago
Merit: An Interpolating Model-Checker
Abstract. We present the tool MERIT, a CEGAR model-checker for safety propf 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. 1 Motivations traction with interpolants (LAWI) [8] is a generic technique to verify the safety of a system. It builds a tree by unwinding the control structure of the sys...
Nicolas Caniart
Added 17 Aug 2010
Updated 17 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Nicolas Caniart
Comments (0)