Static Analysis, Verification

Rosette: About

emina/rosette: The Rosette solver-aided host language, sample solver-aided DSLs, and demos

(159) Synthesis and Verification for All - Emina Torlak - YouTube

UNSAT: Serval

UNSAT: Jitterbug

Cosette: An Automated SQL Solver

Specifying and Checking File System Crash-Consistency Models



Optimizing Synthesis with Metasketches

UW PLSE Neutrons



Synthesizing Evidence of Emergent Computation (SEEC) - Galois, Inc.


EPICS - Experimental Physics and Industrial Control System


anishathalye/notary: Notary: A Device for Secure Transaction Approval ūüďü

mangpo/swizzle-inventor: A framework that helps implementing swizzle GPU kernels

edbutler/nonograms-rule-synthesis: Source code for publication ‚ÄúSynthesizing Interpretable Strategies for Solving Puzzle Games‚ÄĚ from FDG 2017.

jamesbornholt/quivela: Quivela is a prototype tool for constructing proofs of the security of cryptographic protocols.

alanb2718/wallingford: An experimental DSL for handling state and updates, along with constraints, in Rosette.

rosette/sdsl at master · emina/rosette · GitHub

This FTP site

ML Programming


Haskell Programming

Prolog and Logic Programming

Type-safe Formatted IO

Tagless-Final Style

Tagless-Final Cookbook

Generating (mutually) recursive definitions

Scheme Programming

XML and Scheme

Scheme Programming: Miscellanea

Simple Generators

Probabilistic Programming

From walking to zipping, Part 3: Caught in a zipper


Dynamic Binding