Finding Bugs by Testing

Dr. Michael Norrish (Logic and Computation, National ICT Australia.)

DATE: 2005-12-02
TIME: 11:00:00 - 12:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU

ABSTRACT:
I will describe how my colleagues and I have found bugs in real-world TCP/IP and UDP implementations (mainly BSD's but also in Linux and Windows XP) by testing. In more detail, I will describe how such an activity is only possible by first constructing a detailed formal description of what exactly the TCP/IP stack is supposed to be doing in the first place.

Further, because of the presence of significant non-determinism, the task of determining whether or not observed behaviours are in error or not is non-trivial. I will describe the way in which this non-determinism is handled.

BIO:
Dr. Norrish leads the project VNS (Validating Network Semantics) which is a collaboration between NICTA and the University of Cambridge aimed at specifying and analysing the TCP/IP protocols. He is also involved in the L4 Micro-kernel Verification project, in collaboration with researchers from NICTA’s Formal Methods and Embedded and Real-Time Operating System programmes. His particular role in the project is to provide expertise on the semantics of the C programming language.

Dr. Norrish’s research interests include formal methods, interactive theorem-proving, mechanised mathematics and formal semantics. Formal methods are techniques that allow rigorous, logical analysis of computer systems. Such techniques can be used as part of the design of such systems, or in verifying that systems behave as they are supposed to. Dr. Norrish’s work in interactive theorem-proving is centered on the design and development of the HOL theorem-proving system. HOL helps people construct proofs of mathematical theorems; it checks that the users’ proofs are correct, and can also help by automatically bridging “trivial” gaps in proofs. Dr. Norrish’s work in the fields of formal semantics and mechanised mathematics applies the HOL system to problems in theoretical computer science.

Before joining NICTA, Dr. Norrish was a post-doctoral research fellow at St. Catharine’s College in the University of Cambridge for three years. Before holding this position, Dr. Norrish studied for his PhD at Cambridge. He studied for his undergraduate degrees, a BSc(Hons) in Computer Science and a BA in History, at Victoria University of Wellington, in New Zealand.

MEDIA:
051202_norrish.pdf

	Skip Navigation CECS Home \| ANU Home \| Search ANU \| HORUS \| Staff Home
	Seminars @ CECS ANU College of Engineering and Computer Science