 |
|
||||||||||
Spec#
Open Positions
We are recruiting PhD students in program verification, programming languages, and programming environments. Check out the job descriptions.
Our Mailing List
If you are interested in our activities, you can subscribe to the PMInterest mailing list.
Available Student Projects
Our group offers many different topics for Master's theses, Bachelor's theses, and Research in Computer Science Projects.
Spec# is a programming system, which consists of the Spec# programming language, a verification methodology, and a static verifier. The language extends C# with non-null types, method contracts, and object invariants. The verification methodology is based on ownership and allows one to reason about complex heap data structures in the presence of aliasing and call-backs. The static verifier is based on the Boogie verification engine and the automatic theorem prover Z3.
Our current research focus in the Spec# project is the integration of automatic program verification into the development process. For instance, we work on techniques that help programmers to understand and localize verification errors and study how to effectively integrate automatic verification and specification-based testing.
Key Results
The Spec# compiler and verifier are available as open source release. The Spec# tutorial presents Spec# from a programmer’s perspective, whereas our ECOOP 2004 paper explains the core of Spec#’s verification methodology.
Collaboration
Spec# is a collaboration of many people. We have worked mostly with Rustan Leino, Microsoft Research.
Project Members at ETH
Adam Darvas (until 2009)
Joseph Ruskiewicz (until 2011)
Funding
Our work on Spec# is partly funded by the ETH Research Grant TANDEM.
Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne
graphische Elemente dargestellt. Die Funktionalität der
Website ist aber trotzdem gewährleistet. Wenn Sie diese
Website regelmässig benutzen, empfehlen wir Ihnen, auf
Ihrem Computer einen aktuellen Browser zu installieren. Weitere
Informationen finden Sie auf
folgender
Seite.
Important Note:
The content in this site is accessible to any browser or
Internet device, however, some graphics will display correctly
only in the newer versions of Netscape. To get the most out of
our site we suggest you upgrade to a newer browser.
More
information
