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 pageBoogie verification engine. The other, more recent implementation is a frontend to our Viper tool infrastructure and is available on external pageGitHub.
Links
Watch an external pageepisode of Verification Corner
Download external pageViper 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. [DownloadPDF] [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. [DownloadPDF] [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. [DownloadPDF] [BIB] - K. R. M. Leino, P. Müller, and J. Smans: Deadlock-free Channels and Locks
European Symposium on Programming (ESOP), 2010. [DownloadPDF] [BIB] - K. R. M. Leino and P. Müller: A Basis for Verifying Multi-Threaded Programs
European Symposium on Programming (ESOP), 2009. [DownloadPDF] [BIB]
Acknowledgments
Chalice was originally developed in collaboration with external pageRustan 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.