Code-Level Formal Verification for Large Real Systems

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

• Mark Staples (NICTA)
• Wednesday 27 June 2012, 11:00-12:00
• SS03, Computer Lab, William Gates Building.

If you have a question about this talk, please contact Eiko Yoneki.

NICTA has completed the machine-checked, code-level formal verification of the full functional correctness of the seL4 operating system microkernel. This outcome confirms that it is feasible to perform this kind of detailed formal verification in real software engineering projects. However, although seL4 is complex, it is not a very large system (8700 lines of C code).

Our next broad challenge is to make it feasible to complete the code-level formal verification of key security and safety properties 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 with that help to address this broad challenge.

The first area is on better understanding of the software process and management for large-scale formal methods projects. The second area is on approaches to define and analyse software architectures for large trustworthy systems built using trusted and untrusted components. The final area is more methodological and philosophical: how should we establish the empirical validity of the formal models used in formal verification?

Bio: Mark Staples is a Principal Researcher in the Software Systems Research Group at NICTA , and a Conjoint Senior Lecturer at the University of New South Wales. He is conducting research at the borders between software engineering, formal methods, and systems.

Earlier at NICTA he was a member of, then led, NICTA ’s empirical software engineering group. He was the founding leader of the Fraunhofer Project Centre in Transport and Logistics at NICTA , a strategic collaboration between NICTA and Fraunhofer IESE . In conjunction with Fraunhofer IESE and SAP Research, he led the creation of the Future Logistics Living Lab facility and industry network.

Prior to joining NICTA , he worked in the software industry for several years, first on a safety-critical SCADA system, and then on a business-critical web payments infrastructure product. He completed undergraduate degrees in computer science and cognitive science at the University of Queensland, and a PhD on theorem proving and formal methods at the University of Cambridge.

This talk is part of the Computer Laboratory Systems Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• CL's SRG seminar
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Security Seminar
• Computer Laboratory Systems Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• SS03, Computer Lab, William Gates Building
• School of Technology
• Security-related talks
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.