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 available through the Racket package manager:
raco pkg install ocelot
Get the code
Ocelot is available on GitHub.