PSL with its library Prover SL CE is a model checker capable of formally verifying big industrial systems. For valid properties it produces a proof log that can be checked by an independent checker. For falsified properties it produces a counterexample and provides powerful built-in debugging aid.
PSL is the model checker used in Prover Certifier, the full solution for sign-off verification at the level of CENELEC EN 50128 SIL 4.
PSL is also used for the Verifier module of Prover iLock, our full development suite for railway interlocking systems software.
PSL is the successor of our model checkers Tecla, Prover SL and Prover SL DE, that have been widely used during many years in railway applications as well as other domains.
PSL is the choice if performance is important to you. We know of no model checker with similar performance on industrial problems.