This website is about the 2011 edition of the school. Visit this year's edition of LASER.

8th LASER Summer School on Software Engineering


Tools for Practical Software Verification

September 4-10, 2011 - Elba Island, Italy

Edmund Clarke (Carnegie Mellon)
Patrick Cousot (École Normale Supérieure)
Patrice Godefroid (Microsoft Research)
Rustan Leino (Microsoft Research)
Bertrand Meyer (ETH Zurich)
César Muñoz (NASA Langley Research Center)
Christine Paulin-Mohring (Université Paris-Sud)
Andrei Voronkov (University of Manchester)



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 In his spare time, he plays music and teaches cardio exercise classes.

  • Bertrand Meyer, ETH Zürich and Eiffel Software (director)

    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


Chair of Software Engineering - ETH Zurich Last update: 12.08.2011