Prover iLock Verifier provides efficient formal verification of safety requirements against system designs created in Prover iLock. Verification of external code, imported into Prover iLock, is also supported.
Formal verification is based on automatic proof search, and provides 100% verification coverage against forbidden, unsafe states: if the system under verification can reach any state that violates a safety requirement, Prover iLock Verifier detects and reports this, including the sequence of events leading to this state.
The built-in debugger provides efficient support for identifying why the system allows entering a forbidden, unsafe state. Formal verification is strongly recommended for safety verification by standards such as CENELEC EN 50128, and encouraged or even mandated by a growing number infrastructure managers. Prover iLock Verifier provides automated, easy-to-use formal verification with unparalleled speed and capacity, ensuring predictable formal verification results for your interlocking systems.