Truth/SLC

Truth/SLC -- a parallel verification platform for concurrent systems. Concurrent software and hardware systems play an increasing rôle in today’s applications. Due to the large number of states and to the high degree of nondeterminism arising from the dynamic behavior of such systems, testing is generally not sufficient to ensure the correctness of their implementation. Formal specification and verification methods are therefore becoming more and more popular, aiming to give rigorous support for the system design and for establishing its correctness properties, respectively. In view of the inherent complexity of formal methods it is desirable to provide the user with tool support. It is even indispensable for the design of safety-critical concurrent systems where an ad hoc or conventional software engineering approach is not justifiable. There is one particularly successful automated approach to verification, called model checking, in which one tries to prove that (a model of) a system has certain properties specified in a suitable logic