New Racket template: rosette-template rosette-template
A #lang rosette template for program verification and synthesis
(Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. http://emina.github.io/rosette/ )
The template contains many Rosette example files:
synth.rkt: a sample program synthesizer (synthesis query) taken from Building a Program Synthesizer by James Bornholt.
verify.rkt: a sample program verifier (verification query).
sudoku.rkt: a sample Sudoku solver (angelic execution query)
New Racket template: rosette-template
rosette-templateA #lang rosette template for program verification and synthesis
(Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. http://emina.github.io/rosette/ )
The template contains many Rosette example files:
Detailed description is given in each file.
More details at https://github.com/racket-templates/rosette-template