University of Birmingham > Talks@bham > Bravo > Hoare logic and B-Method: How to prove that trains (almost) never collide

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.