BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Mechanical Formalization of Measure\, Integration and Probabil
 ity - David Lester (University of Manchester)
DTSTART:20081021T120000Z
DTEND:20081021T130000Z
UID:TALK13421@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In traditional engineering disciplines - such as mechanical or
  structural engineering - product safety is often described in terms of "m
 ean time between failures". Absolute reliability is either not possible\, 
 or - even where it might be possible - is regarded as too expensive.\n\nIt
  might seem that software engineering is not subject to the same considera
 tions: after all\, software weighs nothing! However\, over-designing the s
 oftware 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 pertin
 ent 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-con
 trol computer are correctly rounded?\n\nHaving a formalized continuous mat
 hematics 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 t
 hen _prove_ that the required probability of the system behaving correctly
  is met. With luck\, this process might be susceptible to\nextensive autom
 ation.\n\nThe talk will assume no specialized knowledge of Probability\, I
 ntegration or Measure\; nor will an extensive knowledge of PVS be assumed.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR