SLAB
Subproject |
R1 |
Categories |
Model checker for hard & soft real-time systems |
Overview |
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. |
K. Dräger, A. Kupriyanov, B. Finkbeiner and H. Wehrheim. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. In Javier Esparza and Rupak Majumdar, editors, Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science (LNCS), pages 271-274, 2010. I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing Abstractions. Fundamenta Informaticae, 89(4):369-392, 2008. I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing Abstractions. In Farhad Arbab and Marjan Sirjani, editors, Proceedings of the International Symposium on Fundamentals of Software Engineering (FSEN), 2007. |
|
Emergency Messages in ETCS, SLAB Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |