Rosette: Solver-aided programming language
Rosette: About

    

Rosette is a solver-aided programming language that extends
Racket with language constructs for program
synthesis, verification, and more. To verify or synthesize code,
Rosette compiles it to logical constraints solved with
off-the-shelf SMT solvers. By combining
virtualized access to solvers with Racket’s metaprogramming, Rosette
makes it easy to develop synthesis and verification tools for new
languages.  You simply write an interpreter for your language in
Rosette, and you get the tools for free!

#lang rosette

(define (interpret formula)
  (match formula
    [`(∧ ,expr ...) (apply && (map interpret expr))]
    [`(∨ ,expr ...) (apply || (map interpret expr))]
    [`(¬ ,expr)     (! (interpret expr))]
    [lit            (constant lit boolean?)]))

; This implements a SAT solver.
(define (SAT formula)
  (solve (assert (interpret formula))))

(SAT `(∧ r o (∨ s e (¬ t)) t (¬ e)))


To learn more, take a look at The Rosette Guide,
this talk,
applications, courses, or publications.

Acknowledgments

This research was supported in part by awards from the National Science
Foundation (NSF CCF 1651225, 1337415, 1139138, and 0916351), the
Department of Energy (DOE DE-SC0005136 and DOE FOA-0000619), and gifts from
Intel, Nokia, and Samsung. Rosette extends the Racket
programming language, and uses the Z3 solver
from Microsoft Research. Many thanks to the authors of these systems for making
them freely available, and to Rosette users for many helpful comments and
suggestions.


  