BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Code-Level Formal Verification for Large Real Systems - Mark Stapl
 es (NICTA)
DTSTART:20120627T100000Z
DTEND:20120627T110000Z
UID:TALK38437@talks.cam.ac.uk
CONTACT:Eiko Yoneki
DESCRIPTION:NICTA has completed the machine-checked\, code-level formal ve
 rification of the full functional correctness of the seL4 operating system
  microkernel.  This outcome confirms that it is feasible to perform this k
 ind of detailed formal verification in real software engineering projects.
 \nHowever\, although seL4 is complex\, it is not a very large system (8700
  lines of C code).\n\nOur next broad challenge is to make it feasible to c
 omplete the code-level formal verification of key security and safety prop
 erties of very large highly-critical software-intensive systems. We expect
  that seL4 will provide a foundation for this. In this talk I will give an
  overview of three areas of recent ongoing  research that I am involved wi
 th that help to address this broad challenge.\n\nThe first area is on bett
 er understanding of the software process and management for large-scale fo
 rmal methods projects. The second area is on approaches to define and anal
 yse software architectures \nfor large trustworthy systems built using tru
 sted and untrusted \ncomponents. The final area is more methodological and
  philosophical:\nhow should we establish the empirical validity of the for
 mal models \nused in formal verification?\n\nBio: Mark Staples is a Princi
 pal Researcher in the Software Systems Research Group at NICTA\, and a Con
 joint Senior Lecturer at the University of New South Wales.  He is conduct
 ing research at the borders between software engineering\, formal methods\
 , and systems.\n\nEarlier at NICTA he was a member of\, then led\, NICTA's
  empirical software engineering group. He was the founding leader of the F
 raunhofer Project Centre in Transport and Logistics at NICTA\, a strategic
  collaboration between NICTA and Fraunhofer IESE.  In conjunction with Fra
 unhofer IESE and SAP Research\, he led the creation of the Future Logistic
 s Living Lab facility and industry network.\n\nPrior to joining NICTA\, he
  worked in the software industry for several years\, first on a safety-cri
 tical SCADA system\, and then on a business-critical web payments infrastr
 ucture product.  He completed undergraduate degrees in computer science an
 d cognitive science at the University of Queensland\, and a PhD on theorem
  proving and formal methods at the University of Cambridge.\n
LOCATION:SS03\, Computer Lab\, William Gates Building
END:VEVENT
END:VCALENDAR