Refinement Types for Rust

Artifact for POPL 2024

Tricks you wish the Coq manual told you [maintainer=@tchajed]

Goose converts a small subset of Go to Coq

DaisyNFS is an NFS server verified using Dafny and Perennial.

Verifying concurrent crash-safe systems

Solve puzzles. Learn CUDA.

The CompCert formally-verified C compiler

Compositional Verification of Composite Byzantine Protocols

isla coq infrastructure

Sail architecture definition language

A lazy clause generation constraint solver written in Rust.

llvm opt fuzzer and bounded exhaustive test generator

Csmith, a random generator of C programs

C-Reduce, a C and C++ program reducer

A JavaScript Engine Fuzzer

Enumerative Testing and Bounded Validation of SMT Solvers

egg is a flexible, high-performance e-graph library

Yet Another Random Program Generator

Recent Fuzzing Paper

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

A randomized program fuzzer for the Rust programming language

Home of OpenVMM and OpenHCL.

Language server for real-time testing diagnostics

HeteroRefactor: Refactoring for Heterogeneous Computing with FPGA

A superoptimizer for LLVM IR

The AI developer platform. Use Weights & Biases to train and fine-tune models, and manage models from experimentation to production.