×

Rosette

swMATH ID: 27566
Software Authors: Torlak, E., Bodík, R.
Description: 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!
Homepage: https://emina.github.io/rosette/
Related Software: GitHub; FlashMeta; Alloy*; Spacer; YACC; Qlose; LLVM; CVC4SY; MiniSat; Paracooba; Kissat; CaDiCaL; Z3str3; COMiniSatPS; JViews; MUSer2; AsmL; Yices; Reveal; Agda
Cited in: 6 Documents

Citations by Year