Formal Verification

Prover PSL®

Prover PSL is an efficient model checker capable of formally verifying big industrial systems. It is known as the model checker on the market.

Prover PSL supports bounded model checking for debugging, as well as many proof strategies, such as simple induction, k-induction, interpolation, IC3 and more. Its noise reduction feature is a highly appreciated method for producing easy-to-understand counterexamples.

Prover PSL

About Prover PSL®

For valid properties, Prover PSL produces a proof log that can be checked by an independent checker from Prover or some other supplier. For falsified properties, Prover PSL produces a counterexample and provides powerful built-in debugging aid.

Prover 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.

Prover PSL is also used in Prover iLock Verifier. Prover iLock is our full development suite for railway interlocking systems software.

Prover PSL is the successor of our model checkers Tecla, Prover SL, Prover SL DE, and Prover SL CE, that have been widely used for many years in railway applications as well as other domains.

Prover PSL is the choice if performance is important to you. We know of no model checker with similar performance on industrial problems.

Try HLL and Prover PSL in our free Prover Station Playground.

New features

Since version 4, Prover PSL support floating point numbers (IEEE 754) and with version 5 came support for the statement-based HLL dialect sHLL, which allows you to model imperative programs in a straightforward way.

Why tool in batch mode. Let your nightly builds produce traces for you to look at in the morning!
Incremental SAT. Find deep counterexamples quicker with the new incremental SAT solving algorithm.
Check that expressions are well defined. Investigate if your system and requirements are well-defined with several built-in checks.
Floating point arithmatic. Prove that your computations are correct according to the standard IEEE 754.
sHLL support allows you to model imperative programs in a more natural and straightforward way.
Multi-file support. Now you can give Prover PSL several HLL and sHLL files to work with simultaneously, allowing cross references.

Prover’s innovative solution bring benefits to many types of Rail Control Projects.

Book A demo

Learn the possibilities with Prover – in action!

Book a 30 minute demo and learn about what benefits Prover products can bring to you and your organisation.

We’ll cover how to:

  • Specific Application Engineering with Prover iLock

  • Formal Verification with Prover iLock and Prover Certifier

Prefer speaking on the phone? Contact us on +46 (0)8 617 68 00.