Rustan Leino

(Microsoft Research, Redmond)

"The Spec# Programming System"

(Vortrag im Rahmen der "Distinguished Lecture Series Spring 2006" des Max Planck Instituts für Software-Systeme)

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.

Zeit:	Montag, 20. März 2006, 14:00 Uhr
Ort:	Gebäude 57, Raum 208/210 (Rotunde)

	Übergeordnete Seite: Jahr 2006
	15 Vorträge

	Feedback
	Email an den Verantwortlichen dieser Seite (sakdapol@informatik.uni-kl.de)