![]() |
![]() |
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 listsTheoretical Physics Seminars Medical Imaging Research Seminars School of Mathematics EventsOther talksMetamaterials for light-matter interaction studies Ultrafast, all-optical, and highly efficient imaging of molecular chirality Geometry of alternating projections in metric spaces with bounded curvature Quantum simulations using ultra cold ytterbium Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems TBC |