The Mechanical Formalization of Measure, Integration and Probability

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

• David Lester (University of Manchester)
• Tuesday 21 October 2008, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.