Chalice
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 design decisions explicit via contracts. The Chalice program verifier checks that the given contracts are never violated and detects other errors such as potential data races and deadlocks.
There were two implementations of Chalice. The original tool was implemented on top of the external page Boogie verification engine. The other, more recent implementation is a frontend to our Viper tool infrastructure and is available on external page GitHub.
Links
Watch an external page episode of Verification Corner
Download external page Viper implementation
Project Members
The project has been completed. Please contact Peter Müller in case of questions or comments.
Key Publications
- S. Heule, I. T. Kassios, P. Müller, and A. J. Summers: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions
European Conference on Object-Oriented Programming (ECOOP), 2013. [Download PDF] [BIB] - S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers: Abstract Read Permissions: Fractional Permissions without the Fractions
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013. [Download PDF] [BIB] - K. R. M. Leino, P. Müller, and J. Smans: Verification of Concurrent Programs with Chalice
Foundations of Security Analysis and Design V, 2009. [Download PDF] [BIB] - K. R. M. Leino, P. Müller, and J. Smans: Deadlock-free Channels and Locks
European Symposium on Programming (ESOP), 2010. [Download PDF] [BIB] - K. R. M. Leino and P. Müller: A Basis for Verifying Multi-Threaded Programs
European Symposium on Programming (ESOP), 2009. [Download PDF] [BIB]
Acknowledgments
Chalice was originally developed in collaboration with external page Rustan Leino, Microsoft Research, and Jan Smans, Katholieke Universiteit Leuven. The project also greatly benefited from work by our previous team member Ioannis Kassios and a student project and further work by Stefan Heule.