Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
The Spec# Programming System
Rustan Leino
Microsoft Research
SWS Distinguished Lecture Series
Dr. Rustan Leino is a researcher at Microsoft Research, where his research centers around programming tools. He is currently working on the design and implementation of the Spec# programming language and its static program verifier. 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 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 at Microsoft.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 20 March 2006
14:00
-- Not specified --
G26
024
Kaiserslautern
Abstract
Spec# is a programming system that aims to provide programmers with a higher degree of rigor than in common languages today. The Spec# language extends the object-oriented .NET language C#, adding features like non-null types, pre- and postconditions, and object invariants. In addition to static type checking and compiler-emitted run-time checks for specifications, Spec# has a static program verifier. The program verifier translates Spec# programs into verification conditions, which are then analyzed by an automatic theorem prover. In this talk, I will give an overview of Spec#, including a demo. I will then discuss some aspects of its design in more detail.
Contact
--email hidden
passcode not visible
logged in users only
Carina Schmitt, 05/10/2006 10:24
Uwe Brahm, 05/09/2006 19:08
Uwe Brahm, 05/09/2006 18:59 -- Created document.
Uwe Brahm, 05/09/2006 19:08
Uwe Brahm, 05/09/2006 18:59 -- Created document.