Prover Certifier

Construct a Formal Correctness Proof of Your System

About Prover Certifier

Prover Certifier is the only sign-off verification tool on the market that allows you to automatically produce complete safety evidence for CENELEC EN50128 SIL 4 certification using formal verification.

Rather than spending resources on time-consuming tasks such as manual reviews and safety testing, with Prover Certifier you construct a formal correctness proof of your system. Not only is the proof completed in a fraction of the time it takes to produce traditional safety evidence, it also provides 100 % coverage as formal verification is guaranteed to discover any error, even those that are extremely hard to find by testing. Since Prover Certifier has been carefully developed in a CENELEC SIL 4 compliant process, its judgment can be fully trusted and can replace other evidence.

There is no need to perform extensive code reviews and safety testing anymore. This saves both time and costs, while minimizing the risk of human error in the review and test process, and reduces the dependency on certified test personnel. The system can be taken into revenue service much earlier and you can be certain that it is safe.

Benefits

  • Automated production of CENENLEC SIL 4 compliant safety evidence.
  • Supports multiple target platforms, programming languages and development processes.
  • Mature and proven formal verification technology.
  • Proven in use for a wide variety of applications, including CBTC, ERTMS, traditional interlockings (both computerized and relay based) and onboard systems.

Prover Trident

Prover Trident is a complete process and tool suite for interlocking design automation. Unlike other point tools, Prover Trident covers the whole life-cycle for interlocking software.

Find out more

PiSPEC

Prover provide software automation solutions that reduce time to market with a factor of upto 10 for commissioning of train control systems, with maintained or improved safety.

Find out more

Prover iLock

Prover iLock is a tool suite for configuration, generation and checking of applications based on PiSPEC IP. Creating revenue service code and V&V results based on simulation and formal safety verification is accomplished using push-button tools.

Find out more