Hoare logic and B-Method: How to prove that trains (almost) never collide

Add to your list(s) Download to your calendar using vCal

• Nicolas Blanco
• Tuesday 18 February 2020, 11:00-12:30
• Room 217, School of Computer Science.

If you have a question about this talk, please contact Nicolas Blanco.

In this talk I introduce you to a method to prove correctness of programs that is used in industry.

First I will give you the core ideas underlying the theory. More precisely I will present a way to talk about specification of (imperative) programs called Hoare logic. I will also discuss how proof obligations can be extracted from such a specification using weakest preconditions.

Then I will introduce a method, the B-method, together with a software, AtelierB, that let you write a program, its specification and prove their correctness, among other properties. It is based on Hoare logic and it is widely use in industry on safety-critical systems mostly in the railway industry and in energy.

Finally I will demonstrate how to use AtelierB on a toy example coming from the railway industry. I will also discuss how to make it more realist to give you a sense on how these programs can quickly become quite complex.

During this talk I will try to share my experience on the challenges that can arise when applying formal methods to real-life complex systems.

This talk is part of the Bravo series.

This talk is included in these lists:

• Bravo
• Room 217, School of Computer Science

Note that ex-directory lists are not shown.