Current version: 2.0.7 [2010-03-04]
Copyright © 2009-2010 Saarland University
SLAB is a certifying model checker for infinite-state concurrent systems. The tool is based on a procedure that interleaves automatic abstraction refinement using Craig interpolation with slicing, which removes irrelevant states and transitions from the abstraction. Given a transition system and a safety property to check, SLAB either finds a counterexample trace or produces a certificate of system correctness in the form of inductive verification diagram.
|[DKFW10]||Klaus Dräger, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems.. TACAS 2010.|
|[BDFH08]||Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. Fundamenta Informaticae, 2008.|
|[BDFH07]||Ingo Brückner, Klaus Dräger, Bernd Finkbeiner, and Heike Wehrheim. Slicing Abstractions. FSEN 2007.|
You can download and use SLAB under the terms of the following LICENSE.