Location: .NET trackTime: 2007-11-14 14.00Level: Advanced
|
|
Rustan Leino, Microsoft Research ,USARustan Leino is a Principal Researcher in the Programming Languages and Methods group at Microsoft Research, Redmond, where his research centers around programming tools. He currently leads the Spec# project, which explores enforceable contracts in object-oriented programming. He works on the design and implementation of the Spec# programming language as well as its static program verifier, called Boogie. He is also involved in a new project to verify C code, which reuses the Boogie tool. Before joining Microsoft Research, Leino worked as a researcher at DEC/Compaq SRC, where among other things he led the Extended Static Checking for Java (ESC/Java) project, a light-weight program checker built on the technology of program verification. His PhD thesis from Caltech (1995) addressed an important specification problem in ESC/Modula-3. Before going to graduate school, Leino worked as a software developer and technical lead in Windows/NT at Microsoft. He has written code that shipped in releases of Windows 3.0, Windows 3.1, and Windows/NT 3.5. In his spare time, he plays and records music, teaches step aerobics, and spends time with his wife and four children.
|
|
Spec#Spec# (http://research.microsoft.com/specsharp  ) is an experimental programming system that seeks to push the envelope in specification and verification technology. The system includes the .NET object-oriented programming language Spec#, which is a superset of the C# language, adding type features like non-null types and contract features like pre- and postconditions and object invariants. The types are checked by the compiler. The contracts are checked dynamically through compiler-inserted run-time checks, and they can also be checked statically using the Spec# automatic program verifier. The system is integrated into Microsoft Visual Studio.
|
