University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > The Mechanical Formalization of Measure, Integration and Probability

The Mechanical Formalization of Measure, Integration and Probability

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

If you have a question about this talk, please contact Thomas Tuerk.

In traditional engineering disciplines – such as mechanical or structural engineering – product safety is often described in terms of “mean time between failures”. Absolute reliability is either not possible, or – even where it might be possible – is regarded as too expensive.

It might seem that software engineering is not subject to the same considerations: after all, software weighs nothing! However, over-designing the software component of a system, such as an aircraft avionics sub-system, can easily lead to over-designed hardware; and this will have an effect on the economic viability of the project. One simple and extremely pertinent example will suffice: how many decimal places need to be set aside for each real number to ensure that all arithmetic operations in a flight-control computer are correctly rounded?

Having a formalized continuous mathematics enables us to specify the correctness of computer control systems in terms of a model for the world in which they operate. One can describe the system of differential equations in which the system operates, and then prove that the required probability of the system behaving correctly is met. With luck, this process might be susceptible to extensive automation.

The talk will assume no specialized knowledge of Probability, Integration or Measure; nor will an extensive knowledge of PVS be assumed.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2021, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity