printlogo
http://www.ethz.ch/index_EN
Welcome
 
print
  

Chalice

Open Positions

We are recruiting PhD students in program verification, programming languages, and programming environments. Check out the job descriptions.

Student Projects Available

Our group offers many different topics for Master's theses, Bachelor's theses, and Research in Computer Science Projects. 

Our Mailing List

If you are interested in our activities, you can subscribe to the PMInterest mailing list.

Workshop on Software Correctness and Reliability

All information on the workshop 2014 can be found here.

The slides and videos of 2013 are available on the workshop website

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

Ioannis Kassios

Peter Müller

Alex Summers

 

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

© 2014 ETH Zurich | Imprint | Disclaimer | 30 January 2014
top