Prover to attend World Congress on formal methods in Porto, Portugal from October 7th to 11th.

We will present our tools for formal verification and modeling at the tool presentation of the 3rd World Congress of Formal Methods.

Prover SL CE (PSL) is a state-of-the-art SAT-based model checker, and the result of Prover’s 30-year-long experience in applying formal verification in industry. PSL is used around the world on large industrial models to certify the safety of mission-critical systems, especially in the railway domain.

Our newest multi-core support (Turbo-threading) allows PSL to handle even larger systems and provides impressive speed-ups. Recently, we have added support for IEEE754 floating point. We are also working on using AI (artificial intelligence) techniques to adapt PSL’s search strategy to specific problems, and we have already obtained significant performance gains that add up to what is delivered by turbo-threading.

Prover Certifier is a solution built on top of PSL, based on diversification and equivalence checking, that can produce complete safety evidence for CENELEC EN50128 SIL 4 certification using formal verification. Prover Certifier has been used in many successful applications around the world; as a standalone solution or linked to our interlocking design automation solution Prover Trident.

The main input to both PSL and Prover Certifier is an HLL model. HLL is itself a declarative, stream-based language, suitable for modeling and expressing temporal properties of discrete-time sequential systems. HLL is becoming an open industry standard.

We hope to see you there!