 |
|
||||||||||
Chalice
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.
Chalice is a language and program verifier that detects bugs in concurrent programs. The Chalice language is a small, class-based language that supports concurrency via threads, monitors, and messages. Developers can make the implicit assumptions about their code explicit via contracts. The Chalice program verifier checks that the given contracts are never violated and detects other errors such as data races and deadlocks. Chalice is implemented in Scala, on top of the Boogie verification engine and the automatic theorem prover Z3.
Key Results
Chalice is available as part of the Boogie open source release. The Chalice tutorial presents Chalice from a programmer’s perspective, whereas our ESOP 2009 paper explains the details of Chalice’s verification methodology.
Collaboration
Chalice is a collaboration with Rustan Leino, Microsoft Research, and Jan Smans, Katholieke Universiteit Leuven.
Project Members at ETH
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
