SLAB
Current version: 2.0.7 [2010-03-04]
Copyright © 2009-2010 Saarland University
Introduction
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.
Publications
| [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. |
Contact
Klaus Dräger <draegerXcsYuni-sbYde> (substitute X by @ and Y by .)
Andrey Kupriyanov <kupriyanovXcsYuni-sbYde> (substitute X by @ and Y by .)
Download
You can download and use SLAB under the terms of the following LICENSE.