The 2004 LASER school brings together six of the best experts in the field, from
Europe, the US and Australia:
Jean-Raymond Abrial, ETH Zurich
Jean-Raymond Abrial is a renowned scientist whose work over many years has
had a profound effect on the development of formal methods and on their
acceptance and use in industry. He is the originator of Z and the developer of
the B method and supporting tools, which provide one of the most practical
frameworks for developing industrial systems so that they can be proved correct
as part of the process.
He is currently working on a new version of B (called Event-B) and its
supporting tool in order to enlarge the application of formal methods beyond
the developmement of Software Systems.
Ernie Cohen, Microsoft Research
Ernie Cohen is a software architect at Microsoft, where he works on the Next
Generation Secure Computing Base (NGSCB). He was previously a research
scientist at Bellcore and a visiting researcher at Microsoft Research, UK. His
primary research interest is in correctness proofs for software.
Erich Gamma, IBM
Erich Gamma is the site lead of the IBM OTI lab in Zurich. He leads the Eclipse
Java Development tools project and is a member of the Eclipse and the Eclipse
Tools project management committees. He is also a member of the Gang of Four,
which is known for their book: Design Patterns - Elements of Reusable
Object-Oriented Software. Erich has paired with Kent Beck to develop JUnit, a
popular testing tool for Java. Erich also paired with Kent Beck to write the
book Contributing to Eclipse: Principles, Patterns, and Plug-ins. Before
joining OTI he was working at Taligent on a never shipped C++ development
environment. Erich started with object-oriented C++ programming over 20 years
ago as a the co-author of ET++ one of the first large scale C++ application
ETH Zurich/Eiffel Software
Bertrand Meyer is Professor of Software Engineering at ETH Zurich and Chief
Architect of Eiffel Software. His current research interests include object
technology, Trusted Components, proofs of classes, object-oriented concurrency.
He is the author of Object-Oriented Software Construction and other
books on software engineering, object technology and programming languages.
University of New South Wales
Carroll Morgan holds an Australian Professorial Fellowship at the University of
New South Wales. He is known mainly for his contributions to Abrial's Z
Specification Technique (early 1980's), his work on the Refinement
Calculus (mid-80's to mid-90's) and most recently for his and his
collaborators' extension of the ideas of specification and refinement to probabilistic
Programming from Specifications and (forthcoming, with Annabelle
Refinement and Proof for Probabilistic Systems summarise many
of his interests; the latter text will be used as the basis for the course.
Currently he is investigating the relationship between probabilistic choice,
angelic- and demonic nondeterminism in the context of concurrent systems and of two-player games.
Pamela Zave received the Ph.D. degree in computer sciences from the University
of Wisconsin-Madison. She taught at the University of Maryland before joining
AT&T Bell Laboratories in 1981. She is now a Technology Advisor in the
Information and Software Systems Research Laboratory of AT&T.
Dr. Zave's chief interests are requirements engineering and formal methods for
software development. She is best known for her work on multiparadigm
specification, the executable specification language PAISLey, and the
Distributed Feature Composition architecture. In 2002 she was named a Fellow of
the ACM for her contributions to the use of formal methods in telecommunication
software. She holds many patents in the area of telecommunications.
Dr. Zave is an associate editor of ACM Transactions on Software Engineering and
Methodology, and a member of IFIP Working Group 2.3 (Programming Methodology)
and IFIP Working Group 2.9 (Requirements Engineering). She has served on the
program committees of many conferences, including chairing the program
committee of the Second IEEE International Symposium on Requirements
Engineering, and co-chairing the program committee of Formal Methods Europe