The 2011 LASER school brings together some of the best experts in the field :
- Edmund Clarke, Carnegie Mellon
Edmund M. Clarke, recipient of the 2007 Turing Award, received a B.A. degree in mathematics from the University of Virginia, Charlottesville, VA, in 1967, an M.A. degree in mathematics from Duke University, Durham NC, in 1968, and a Ph.D. degree in Computer Science from Cornell University, Ithaca NY, in 1976. After receiving his Ph.D., he taught in the Department of Computer Science, Duke University, for two years. In 1978 he moved to Harvard University, Cambridge, MA where he was an Assistant Professor of Computer Science in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie-Mellon University, Pittsburgh, PA. He was appointed Full Professor in 1989. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008.
- Patrick Cousot, École Normale Supérieure
Patrick Cousot is Professor of Computer Science.
He was appointed, in France at the École Normale Supérieure (ENS, 1991), Paris, France where he is Director of the Computer Science educational activities and leads the research on abstract interpretation and semantics (ENS-CNRS-INRIA joint project team "Abstraction"); the École Polytechnique (X, 1984-1997), where he developped the educational activities in Computer Science and created and headed the research laboratory (LIX) and the University of Metz (1979-1984). He was appointed, in the US, at New York University (NYU, 2008); the Massachusetts Institute of Technology (MIT, 2005) as J. C. Hunsaker Distinguished Visiting Professor.
Before, Patrick Cousot was Research Scientist at the French National Center for Scientific Research (CNRS, 1974-1979), at the University of Grenoble.
Patrick Cousot is Engineer from École des Mines of Nancy (1971), Doctor Engineer (PhD) in Computer Science (1974) and Doctor ès Sciences in Mathematics (1978) from the University of Grenoble.
Patrick Cousot is the inventor with Radhia Cousot, of Abstract Interpretation (1975). Abstract interpretation is a theory of sound approximation of mathematical structures, in particular those involved in the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model-checking, static analysis, program transformation and optimization, typing, software steganography, etc.). Its current main industrial application is on the safety and security of complex hardware and software computer systems.
Patrick Cousot was named Chevalier (knight) in the Ordre des Palmes académiques (1990) and in the Ordre National du Mérite (1993). He was awarded the Silver Medal of the CNRS (1999), an honorary doctorate from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), the Grand Prix of Computer Science and its Applications of the EADS Corporate Research Foundation attributed by the French Academy of Sciences (2006) and a Humboldt Research Award (2008). He is Member of the Academia Europaea (2006).
- Patrice Godefroid, Microsoft Research
Patrice Godefroid is a Principal Researcher at Microsoft Research. He
received the B.S. degree in Electrical Engineering (Computer Science
elective) and the Ph.D. degree in Computer Science from the University
of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006,
he worked at Bell Laboratories (part of Lucent Technologies), where he
was promoted to "distinguished member of technical staff" in 2001. His
research interests include program (mostly software) specification,
analysis, testing and verification.
Dr. Godefroid is probably best known for his pioneering work on
partial-order reduction for model checking concurrent systems (his PhD
thesis is published as LNCS volume 1032 by Springer), for his work on
VeriSoft, the first software model checker for mainstream programming
languages such as C and C++, for his work on 3-valued model checking
with may/must abstractions for sound program verification and
falsification, and for his work on automatic test generation with
DART. More recently, he co-developed SAGE, the first whitebox fuzzer
for security testing, which was credited to have found roughly one
third of all the security vulnerabilities discovered by file fuzzing
during the development of Microsoft's Windows 7.
- Rustan Leino, Microsoft Research
Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research. He is known for his work on programming methods and program verification tools. At Microsoft Research, he has led the Spec# project, which brings enforced pre- and post-conditions to the .NET platform, and is the architect of the Boogie program verification framework, which underlies several program verifiers for Spec#, C, and other languages. Previously, Leino led the ESC/Java project at Compaq SRC and worked on specifications on the pioneering ESC/Modula-3 project at DEC SRC.
Before getting his PhD (Caltech, 1995), Leino wrote and designed object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and has recently started the Verification Corner video show on channel9.msdn.com. In his spare time, he plays music and teaches cardio exercise classes.
ETH Zürich and Eiffel Software
Bertrand Meyer is Professor of Software Engineering at ETH Zürich and Chief
Architect of Eiffel Software. His current research interests include object
technology, proofs and tests of classes, object-oriented concurrency.
- César Muñoz, NASA Langley Research Center
César Muñoz earned an Engineering and a Master degree in Computer Science from the Universidad de los Andes (Bogotá), and a M.Sc. and Ph.D. in Computer Science from the University of Paris 7 (Paris).
He was a Research Assistant in the Coq team at INRIA (Rocquencourt). After completing his Ph.D., he spent one and a half years as an International Fellow in the Computer Science Laboratory at SRI International (formerly, Stanford Research Institute) in Menlo Park.
In 1999, he joined the Formal Methods group at ICASE - NASA Langley. From 2003 to 2008, he worked for the National Institute of Aerospace at Langley Research Center, where he led the NIA Formal Methods group.
Since 2009, César Muñoz is a Research Computer Scientist at NASA.
- Christine Paulin-Mohring, Université Paris-Sud
Christine Paulin-Mohring is a Professor at Université Paris-Sud 11
since 1997. She obtained her PhD in 1989 from Université Paris 7,
working under the supervision of Gérard Huet at INRIA Rocquencourt and
Ecole Normale Supérieure on the early version of the Calculus of
Constructions. She spent 8 years as a CNRS Researcher at Ecole Normale
Supérieure in Lyon, where she contributed to the development of the
Coq proof assistant especially on the aspects concerning inductive
definitions and program extraction. She is currently leading a
research group ProVal (INRIA Saclay - Île-de-France, Université
Paris-Sud and CNRS) on the use of proof technology for developing
correct programs. While using the Coq proof assistant to validate
functional programs or build complex theories, the ProVal group also
develops extended tools such as the Why platform to analyse programs
with imperative features and make use of powerful automated theorem
provers such as SMT solvers.
- Andrei Voronkov, University of Manchester