What is new in Prover PSL 6.0? 

Reachability obligations – a new way to strengthen verification 

Prover PSL 6.0 introduces reachability obligations, a new type of verification check that complements traditional proof obligations. This feature allows you to verify whether specific states can be reached in your model, helping to refine system validation and efficiently identify edge cases. (Requires an add-on) 

HLL and sHLL simulation in Why tool 

Now, you can simulate HLL and sHLL models directly in the Why Tool. This integration enables step-by-step execution, making it easier to debug, analyze counterexamples, and validate expected behaviors — all within a unified environment. (Requires an add-on) 

Enhanced proof analysis with coverage and profiling 

Prover PSL 6.0 introduces two new analysis options for greater proof transparency: 

• A proof coverage analysis to identify which parts of your model are covered during verification, allowing you to optimize proof efficiency. 

• A profiling and performance optimization feature to gain insights into computational bottlenecks by tracking solver workload distribution. 

Greater flexibility with -move for softening constraints 

A new command-line switch allows you to dynamically move constraints, proof obligations, and other model elements between different HLL sections. This flexibility helps refine proof strategies and understanding of your model without modifying the core model structure. 

With Prover PSL 6.0, you gain enhanced debugging, deeper proof coverage insights, and improved solver performance—all designed to push your formal verification process to the next level. 

Upgrade to Prover PSL 6.0 today and elevate your formal verification process!

Inlägget Prover PSL 6.0 released – Reachability obligations along with HLL and sHLL simulations are new features dök först upp på Prover - Engineering a Safer World.

We provided them with an understanding of what an interlocking is, along with initial knowledge about railway systems. Equipped with this basic understanding, we tasked them with debugging an interlocking system using fundamental signaling principles. Following this initial step, the students were empowered to introduce new safety requirements and test cases. In the end, they could incorporate a new manual release feature into their interlocking system, covering aspects such as design, safety requirements, and testing.

We extend our greatest appreciation to the dedicated students of CentraleSupélec for their commitment and enthusiasm throughout the past week. All of them really impressed us with how quickly you got the hang of our tools, languages, and the whole railway field. Our thanks also go to their teachers, in particular Idir Ait Sadoune, who have renewed their confidence in us again for this year.

We are hoping to have the opportunity to see these talented students again in the railway industry or in the field of formal methods. We believe that opportunities to introduce these two fields to new students are essential. We are convinced that this new generation of talents can contribute to the development of these two exciting fields for engineering a safer world.

Inlägget CentraleSupélec collaboration: Students dive into railway projects dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Prover Studio now supports HLL dök först upp på Prover - Engineering a Safer World.

Les prochaines étapes consisteront à convenir concrètement de la définition précise de la future version du langage HLL, les fonctionnalités à ajouter ayant déjà été définies. Nous avons également quelques détails à régler concernant la structure juridique du forum HLL.

Prover souhaite remercier tous les participants pour leurs propositions et leurs commentaires quant à la manière d’organiser le Forum HLL à l’avenir.

Prover est également particulièrement reconnaissant envers IKOS Consulting qui nous a accueillis dans les meilleures conditions pour une journée sereine et efficace.

Inlägget HLL Forum franchit une étape dans la création d’une définition officielle du langage HLL 3.0! dök först upp på Prover - Engineering a Safer World.

The next steps will be to concretely agree about the precise definition of the next version of the HLL language, the features to be added having already been decided. We also have a few details to sort out about the legal structure of the HLL Forum.

Prover would like to thank all participants for their proposals and comments about how to organize the HLL Forum in the future.
Prover is also particularly grateful to IKOS Consulting who welcomed us in the best conditions to a serene and efficient day.

Inlägget HLL Forum takes the step of creating an official language definition for HLL 3.0! dök först upp på Prover - Engineering a Safer World.