Talk "Refinement strategies for correct by construction algorithms"

by Dominique Méry

Fri, 01 November 2024 at 11:30 am in Crete, Greece

Abstract: In this talk, we recall the refinement strategies developed in the context of the Event-B language. The strategies aim to construct correct algorithms by verifying the refinement steps with the Rodin platform. The aim is to show the possibilities offered by these strategies for constructing algorithms or reconstructing classic algorithms from sequential algorithms, and also to demonstrate the verification of such algorithms using contracts and annotations.