A Solver-Aided Relational Logic DSL

Ocelot provides an embedding of relational logic (like Alloy) in the Rosette solver-aided programming language. The embedding allows both solving and verification of relational specifications, as well as synthesis of relational specifications, and integration with other Rosette constraints.

Ocelot’s synthesis support is the key to our MemSynth project for synthesizing memory consistency model specifications.

Ocelot is developed at the University of Washington by James Bornholt and Emina Torlak.

Check out this demo code: axioms.rkt, repair.rkt.

Getting started

Ocelot is available through the Racket package manager:

raco pkg install ocelot

The documentation provides a quick start guide to constructing Ocelot programs. Ocelot is similar to Alloy, and so many of the principles and examples from that language will translate well.

Get the code

Ocelot is available on GitHub.