BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal Methods for Critical Systems - Steve Miller (Rockwell Colli
 ns)
DTSTART:20080918T130000Z
DTEND:20080918T140000Z
UID:TALK13430@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Formal methods have traditionally been reserved for systems wi
 th requirements for extremely high assurance. However\, the growing popula
 rity of model-based development\, in which models of system behavior are c
 reated early in the development process and used to auto-generate code\, a
 re making precise\, mathematical specifications much more common in indust
 ry. At the same time\, formal verification tools such as model checkers co
 ntinue to grow more powerful. The convergence of these two trends opens th
 e door for the practical application of formal verification techniques ear
 ly in the life cycle for many systems. This talk will describe how Rockwel
 l Collins has applied both theorem proving and model checking to commercia
 l avionics and security systems to reduce costs and improve quality.\n\n\n
 \n*Biography for Steven P. Miller*\n\nDr. Steven Miller is a Senior Princi
 pal Software Engineer in the Advanced Technology Center of Rockwell Collin
 s. He has over 30 years of experience in software development for both mai
 nframe and embedded systems. He received his Ph.D. in computer science fro
 m the University of Iowa in 1991\, and also holds a B.A. in physics and ma
 thematics from the University of Iowa.\n\nHis current research interests i
 nclude model-based development and formal methods. He was principle invest
 igator on a 5-year project sponsored by NASA Langley’s Aviation Safety P
 rogram and Rockwell Collins to investigate advanced methods and tools for 
 the development flight critical systems. Prior to that he lead several res
 earch efforts at Rockwell Collins\, including a collaborative effort with 
 SRI International and NASA to formally verify the microcode in the AAMP5 a
 nd AAMP-FV microprocessors using the PVS verification system. \n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR