Static Analysis, Verification

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

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

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

yunshengtw/scftl

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

Haskell Programming

Prolog and Logic Programming

Type-safe Formatted IO

Tagless-Final Style

Tagless-Final Cookbook

Generating (mutually) recursive definitions

Scheme Programming

Scheme Programming: Miscellanea

Simple Generators

Probabilistic Programming

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

https://okmij.org/ftp/Scheme/callcc-fixpoint.txt

Dynamic Binding