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 are two implementations available for Chalice. The original tool was implemented on top of the Boogie verification engine and is available as source and binary releases. The other, more recent implementation is a frontend to our Viper tool infrastructure and is also available for download.
- 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. [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. [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. [PDF] [BIB]
- K. R. M. Leino, P. Müller, and J. Smans: Deadlock-free Channels and Locks
European Symposium on Programming (ESOP), 2010. [PDF] [BIB]
- K. R. M. Leino and P. Müller: A Basis for Verifying Multi-Threaded Programs
European Symposium on Programming (ESOP), 2009. [PDF] [BIB]
Chalice was originally developed in collaboration with 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.