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!
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
We are seeking an Office Coordinator to our Stockholm office.
The Office Coordinator plays a key role in ensuring that our office operates efficiently and in line with Prover’s standards of professionalism and quality. The role combines office management with broad administrative support to management and staff.
The Open signaling Initiative is transforming how railway and metro signaling systems are delivered.
By combining modular technology, collaboration, and open standards, it reduces vendor lock-in, cuts lifecycle costs, and creates space for innovation.
The Open signaling Initiative is transforming how railway and metro signaling systems are delivered.
By combining modular technology, collaboration, and open standards, it reduces vendor lock-in, cuts lifecycle costs, and creates space for innovation.
