Explore @uwplse Open Source projects

UW PLSE (@uwplse)

uwplse

Stars
1,786
Global Org. Rank 10,107 (Top 4 %)
Registered almost 11 years ago
Most used languages

Coq 24.5 %

OCaml
12.2 %

Racket
10.2 %

Java
10.2 %

Rust
8.2 %

HTML
6.1 %

OpenSCAD 4.1 %

C
4.1 %

Shell
2.0 %

Python
2.0 %

Clojure
2.0 %

C++
2.0 %

JavaScript
2.0 %

TeX
2.0 %

Perl
2.0 %

Haskell
2.0 %

Alloy 2.0 %

Jupyter Notebook
2.0 %
Location 🇺🇸 United States
Country Total Rank 5,632
Country Ranking

Alloy 2

Coq 3

Racket
25

OpenSCAD 41

OCaml
59

Clojure
527

Rust
553

C
2,024

Java
2,663

Haskell
2,834

TeX
3,142

Perl
3,711

C++
7,659

Shell
8,087

verdi

A framework for formally verifying distributed systems implementations in Coq

verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

tensat

Re-implementation of the TASO compiler using equality saturation

ruler

Rewrite Rule Inference Using Equality Saturation

Cassius

A CSS specification and reasoning engine

herbgrind

A Valgrind tool for Herbie

crust

A compiler from Rust to C, and a checker for unsafe code

PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

Casper

A compiler for automatically re-targeting sequential Java code to Apache Spark.

pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

szalinski

Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

CoqAST

Fun plugin to play with the Gallina AST.

oddity

A graphical, time-traveling debugger for distributed systems

cheerios

Formally verified Coq serialization library with support for extraction to OCaml

dexter

a compiler for re-writing image processing functions in C++ to Halide

synapse

Optimizing Synthesis with Metasketches, POPL 2016

StructTact

Coq utility and tactic library.

memsynth

An advanced automated reasoning tool for memory consistency model specifications.

rake

compiling DSLs to high-level hardware instructions

stng

compiler for fortran stencils using verified lifting,

oeuf

gallina frontend for CompCert

ferrite

Ferrite, a toolkit for developing file system crash-consistency models

potpie

Proof Object Transformation, Preserving Imp Embeddings: the first proof compiler to be formally proven correct

reincarnate-aec

Reincarnate Artifact for ICFP 2018

magic

Demystifying the magic of supertactics

arvo

A proof assistant.

coq-plugin-lib

Library of useful utility functions for Coq plugins

SaltShaker

Verifying x86 semantics

concerto

Combined concrete and abstract interpretation

crimp

Certified Relational to Imperative

analytics-data

incarnate-exploration-archive

PL for 3D Printing

peek

Peek: a verified peephole optimizer for CompCert

iag-synthesis

Parallel, incremental evaluation of attribute grammars through synthesis

bagpipe

Reasoning about BGP configurations. Public development repo.

theia

Automatically Visualizing Program Execution

fix-to-elim

Fixpoint to eliminator translation in Coq

coq-change-analytics

REPLICA: REPL Instrumentation for Coq Analysis

scout

Using High-Level Design Constraints to Automatically Generate Design Alternatives

Jupyter Notebook

syncro

Synthesis of Incremental Operations

legato

Legato is a static analysis for finding bugs in dynamic resource usage

univalent-rewrites

POPL 2020 PUMPKIN/DEVOID submission

staccato

Stale Configuration and Consistency Analysis Tool

pumpkin

Public webpage for Pumpkin Patch

VeriCQ

Use SpaceSearch to verify Conjunctive Query Rewrite Rules

epics-tools

Static analysis tools for EPICS

PUMPKIN-git

A prototype PUMPKIN PATCH interface with Git integration

seguard-resources

SeGuard Public Resources

nightly-conf

The public nightly server configuration

majortom

An Oddity shim for "arbitrary" x86-64 Linux binaries