DavePearce
Author of the Whiley programming language. Researcher in Smart Contracts @ ConsenSys. Interests include formal verification, compilers, and static analysis.
ConsenSysNew Zealand
Pinned Repositories
DynamicTopologicalSort
C++ code accompanying the paper "A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs".
FeatherweightRust
Provides a reference implementation of FeatherweightRust in Java.
JavaAVR
Simple AVR simulator written in Java
jkit
Java Compiler Kit (JKit)
JModelGen
A model generator library for use with automated test generation.
jx86
Java Library for Generating x86 Code
LeanEVM
A toy implementation of the EVM in Lean4.
SimpleVirtualMachine.wy
A demonstration of how Whiley can be used to verify compiler optimisations on a simple bytecode language.
StronglyConnectedComponents
An example implementation of my algorithm for finding Strongly Connected Components.
TuttePolynomial
Tutte Polynomial Computation
DavePearce's Repositories
DavePearce/DynamicTopologicalSort
C++ code accompanying the paper "A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs".
DavePearce/LeanEVM
A toy implementation of the EVM in Lean4.
DavePearce/SimpleVirtualMachine.wy
A demonstration of how Whiley can be used to verify compiler optimisations on a simple bytecode language.
DavePearce/TuttePolynomial
Tutte Polynomial Computation
DavePearce/EvmTools
Various utilities for working with the Etherem Reference Tests.
DavePearce/SyntacticHeap.rs
A generic data structure designed for representing Abstract Syntax Trees.
DavePearce/BettingContract
A simple betting smart contract written in Solidity.
DavePearce/Conway.wy
An HTML5 Canvas Implemetation of Conway's Game of Life written in Whiley
DavePearce/DevmProofGen
Dafny Evm Proof Generator (experimental)
DavePearce/Homepage
My personal homepage.
DavePearce/Minesweeper.wy
Implementation of Minesweeper in Whiley
DavePearce/SemanticSubtyping
A proof of the semantic subtyping relation from an academic paper.
DavePearce/TokenContract.wy
A simple smart contract written in Whiley.
DavePearce/BigNum.wy
A library providing implementations for unbound integers.
DavePearce/Clink.rs
A Cell-like structure for maintaining type-level invariants.
DavePearce/DeltaInc.rs
A library for describing delta transformations and incremental computation.
DavePearce/DerivationTree
Utilities for describing proof derivations.
DavePearce/evm-dafny
An EVM interpreter in Dafny
DavePearce/Lexington
Parser library
DavePearce/LZ.wy
Library for handling LZ77 and LZW compression and decompression.
DavePearce/PolyLog
Utilities for working with Polynomials
DavePearce/R1csViewer
A simplistic viewer for Rank 1 Constraint Systems written in Rust.
DavePearce/RFCs
Request for Comment (RFC) proposals for substantial changes to the Whiley language.
DavePearce/Stutter.rs
A library describing computation which can be divided into small steps.
DavePearce/TinyFL
A simple example illustrating the Z3 bindings for Rust. The purpose of this is to gain experience working directly with Z3.
DavePearce/TutteCheck
Tools for checking the output of a Decomposed Tutte Computation
DavePearce/VcGen
A simple library for manipulating and generating verification conditions.
DavePearce/WhileyFile.rs
An API written in Rust for parsing Whiley files and more!
DavePearce/WhileyTestFile
A library for parsing Whiley test files.
DavePearce/WhileyWeb.rs
A Rust port of the WhileyWeb system. This allows Whiley programs to be edited, compiled and executed from a single webpage.