The Rosette Language

Acknowledgments

This research was supported in part by awards from the Department of Energy (DOE DE-SC0005136 and DOE FOA-0000619) and the National Science Foundation (NSF CCF-0916351, NSF CCF-1139138, and NSF CCF-1337415), as well as gifts from Intel, Nokia, and Samsung.

Rosette extends the Racket programming language, and it uses the Z3 solver from Microsoft Research. Many thanks to the authors of these systems for making them freely available. Sincere thanks also to the users of Rosette for many helpful comments and suggestions.