PSL – Prover SL CE
About PSL – Prover SL CE
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.
New in version 4
We are happy to announce a new version of PSL, now with support for floating point numbers (IEEE 754) and even better performance! Floating point numbers have been requested for a long time by customers who want to formally verify onboard systems.
Besides floating point numbers you also get several other useful features in PSL 4:
- Why tool in batch mode. Let your nightly builds produce traces for you to look at in the morning!
- Well-definedness checks. Investigate if your system and requirements are well-defined with several built-in checks.
- Incremental SAT. Find deep counterexamples quicker with the new incremental SAT solving algorithm.
- Lots of other useful improvements such as more detailed error messages and new options.