神刀安全网

Rosette: a solver-aided programming language that extends Racket

About Rosette: a solver-aided programming language that extends Racket

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 atThe Rosette Guide,applications, or publications:

  • [1] Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. PLDI 2014. ( ACM , PDF )
  • [2] Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. Onward! 2013. ( ACM , PDF )

转载本站任何文章请注明:转载至神刀安全网,谢谢神刀安全网 » Rosette: a solver-aided programming language that extends Racket

分享到:更多 ()

评论 抢沙发

  • 昵称 (必填)
  • 邮箱 (必填)
  • 网址
分享按钮