![]() |
![]() |
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 collideAdd 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. This talk is included in these lists:Note that ex-directory lists are not shown. |
Other listsCondensed Matter Group Meetings BritGrav 15 Speech Recognition by Synthesis SeminarsOther talksUltrafast Spectroscopy and Microscopy as probes of Energy Materials Horizontal Mean Curvature Flow and stochastic optimal controls Hunt for an Earth-twin Quantum Sensing in Space Counting cycles in planar graphs TBA |