Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more.

Notes related to Rosette solver

Serval solver-based verifier, Verification performance of code, Verification profiling of code, Verifier performance

Papers related to Rosette solver

• Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
• Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
• Growing solver-aided languages with Rosette [torlak:onward:2013]
• A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
• SpaceSearch: A library for building and verifying solver-aided tools [weitz:icfp:2017]
• Solver aided reverse engineering of architectural features [zorn:iscawddd:2017]