Ernie Cohen: Validating the Microsoft Hypervisor
I'll describe a number of ways in which we're using formal methods to specify and validate the Microsoft Hypervisor (a small software layer that partitions a PC into a number of virtual machines). These methods include automatic test generation, an "optimal" form of stateless search, and correctness proofs for MMU virtualization.
About the speaker: Ernie Cohen is a Test Architect at Microsoft, where he develops formal methods for system software and security. Since his PhD at the University of Texas at Austin, he has worked as a Senior Scientist at Bellcore/Telcordia, and a Visiting Researcher and Software Architect at Microsoft.
Nicholas Griffin: Bertrand Russell: A Philosophy for Formal Methods and a Formal Method for Philosophy
This is a general and informal talk about Russell's work in logic and the foundations of mathematics in the early years of the twentieth century. It will focus on the philosophical views which underlay his attempts to solve the Russell paradox (and several others) which culminated in the ramified theory of types. It will also argue that one of his most important contributions to philosophy, was his forcing philosophers to take the new mathematical logic seriously - something that previous practitioners had been unable to do. I will also draw attention to the wealth of material related to Russell's work in logic and philosophy in the Bertrand Russell Archives.
About the speaker: Nicholas Griffin is Director of the Bertrand Russell Research Centre at McMaster University where he holds a Canada Research Chair in Philosophy. He has written extensively on most aspects of Russell's life and work, most recently editing The Cambridge Companion to Bertrand Russell (2003). He is the general editor of The Collected Papers of Bertrand Russell.
Thomas A. Henzinger: Embedded
Systems Design Challenge
We summarize some current trends in embedded systems design and
point out some of their characteristics, such as the chasm between
analytical and computational models, and the gap between
safety-critical and best-effort engineering practices.
We call for a coherent scientific foundation for embedded systems
design, and we discuss a few key demands on such a foundation:
the need for encompassing several manifestations of heterogeneity,
and the need for constructivity in design.
We believe that the development of a satisfactory Embedded Systems
Design Science provides a timely challenge and opportunity for
reinvigorating computer science.
(Joint work with Joseph Sifakis.)
About the speaker: Tom Henzinger is a Professor of Computer and Communication Sciences at EPFL in Switzerland. He holds a PhD degree in Computer Science from Stanford University. He was an Assistant Professor of Computer Science at Cornell University, a Professor of Electrical Engineering and Computer Science at the University of California in Berkeley, and a Director of the Max-Planck Institute for Computer Science in Saarbrüecken. His research focuses on modern systems theory, especially formalisms and tools for the design and verification of software and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems.
Peter Lindsay: Distributed Control in Network-Based Systems
Complex computer-based systems play a critical role in the modern world.
Thanks to advances in Information and Communications Technology, the world
is becoming one huge interlinked system. But as the systems get larger and
increasingly distributed, it is getting increasingly difficult to understand
how they work, and what causes them to fail. It is now increasingly common
to hear talk of "emergent properties" - that is, properties of systems which
are difficult, if not impossible, to predict simply from the properties of
their components. An increasingly important issue for software and system
engineers is, what methods and tools can be used to help understand, manage
and/or design such systems.
Biologists, economists and sociologists have been studying these kinds of
problems for a long time, and have built up a substantial body of knowledge.
Complex Systems Science is the discipline concerned with understanding how
macro-level system properties and behaviours emerge from relatively simple
micro-level interactions. The challenge is how to capture this knowledge in
a form suitable for engineered systems.
This talk will describe new research in modelling and simulation of complex
systems in areas including genetics, plant growth and air traffic control.
About the speaker: Professor Peter Lindsay is Boeing Chair in Systems Engineering in the School of Information Technology & Electrical Engineering at the University of Queensland in Brisbane Australia, and Director of the ARC Centre for Complex Systems (www.accs.edu.au). Professor Lindsay joined the University of Queensland in 1991 after holding academic and research positions at the University of New South Wales and the University of Manchester. He holds an MSc from University of Melbourne and a PhD in mathematical logic from the University of Illinois at Urbana-Champaign. He has twenty years experience in formal aspects of systems and software engineering. He is co-author of two books on formal specification and verification of software systems, and many refereed papers. In recent years he has provided system safety expertise to government and industry on a large number of safety-critical applications in the areas of defence, aerospace and transport. He is a Fellow of the Australian Computer Society.
George Necula: Data Structure Specifications via Local Equality Axioms
We describe a program verification methodology for specifying global
shape properties of data structures by means of axioms involving
arbitrary predicates on scalar fields and pointer equalities in the
neighborhood of a memory cell. We show that such local invariants are
both natural and sufficient for describing a large class of data
structures. We describe a complete decision procedure for such a class
of axioms. The decision procedure is not only simpler and faster than in
other similar systems, but has the advantage that it can be extended
easily with reasoning for any decidable theory of scalar fields.
About the speaker: George Necula is an Associate Professor in the Computer Science Department at University of California, Berkeley. His research interests include programming languages, verification methods and security with an emphasis towards use of programming language and logic-based technologies for security and for improving software quality. George Necula has received his BS in 1993 from Polytechnic University of Bucharest in Romania, and his PhD in Computer Science in 1998 from Carnegie Mellon University, where he developed the technique of Proof-Carrying Code, jointly with Peter Lee. George Necula is an Okawa Fellow, an Alfred P. Sloan Foundation Fellow, a recipient of the NSF Career Award and of the 2001 ACM Grace Murray Hopper Award.