Formal Verification
Prover PSL®
Prover PSL is an efficient model checker capable of formally verifying big industrial systems. It is known as the leading 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.
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.
Abilities
Prover PSL comes with a powerful default strategy which is sufficient for many model checking tasks. You can also choose strategies such as BMC, k-induction, interpolation, IC3. Strategies can be combined in various ways, including by strategy fusion which allows you to let several strategies work together on a given problem.
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.
Add-on: Floating point arithmatic. Prove that your computations are correct according to the standard IEEE 754. Contact us to purchase this ability.
Embedded simulation tool. Step through your HLL and sHLL models interactively. Debug and validate behavior using built-in execution tracing and inspection.
Add-on: sHLL support allows you to model imperative programs in a more natural and straightforward way. Contact us to purchase this ability.
References
Prover’s innovative solution bring benefits to many types of rail control projects
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
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:
Prefer speaking on the phone? Contact us on +46 (0)8 617 68 00.
+46 (0)8 617 68 00