The Rosette Language

Applications

Rosette hosts many domain-specific languages (DSLs) with advanced programming tools that scale to real-world applications, from verification of radiotherapy software to synthesis of code for ultra-low power hardware. Several of these tools have been developed by first-time users of Rosette in just a few days or weeks.

Bagpipe A language for specifying BGP policies and verifying that an Internet Service Provider’s router configurations implement these policies.
Chlorophyll A synthesis-aided programming model and compiler for GreenArrays GA144, a minimalist low-power spatial architecture.
Cosette A framework for reasoning about SQL equivalences.
Ferrite A framework for specifying and checking file system crash-consistency models.
Greenthumb A framework for constructing superoptimizers.
MemSynth A language and tool for verifying, synthesizing, and disambiguating memory consistency models.
Neutrons A verifier for a subset of EPICS. Currently in use at the University of Washington Clinical Neutron Therapy System.
Synapse A framework for specifying and solving optimal synthesis problems.
Ocelot An engine for solving, verifying, and synthesizing specifications in bounded relational logic.
Wallingford An experimental constraint reactive programming language.
More Demo languages and tools for secure stack machines, data-parallel programing, and web-scraping.