Software

This page describes my past and present open source academic software projects.

Verifiably Safe Reinforcement Learning Framework

A framework for applying formal methods to end-to-end reinforcement learning systems.

VSRL Github repo

KeYmaera X

I am a primary developer of KeYmaera X, a theorem prover for hybrid systems. Hybrid systems are a type of dynamical system with both continuous dynamics (differential equations) and discrete dynamics (imperative programs). These systems are often used to model systems in which the specification of a piece of softwawre is intimately related to a continuous phenomenon; for example, KeYmaera X has been used to verify models of self-driving cars, aircraft collision avoidance protocols, and surgical robots.

Teaching tools

• KeYmaera I is a fork of KeYmaera X supporting Intuitionistic Logic. The prover is used for teaching a course in constructive logic at Carnegie Mellon University. The course website contains more information, and the source code is available on GitHub

• My simple discrete predator/prey simulator was used for a lab in the University of Pittsburgh’s undergraduate Mathematical Biology course. Available online

• I developed a simple web simulation of adaptive cruise control to be used as a teaching tool in introductions to verification of cyber-physical systems.

A Type System for String Analysis

I developed a type system that helps reduce errors in security-critical input validation logic as a type system extension in Cyrus Omar’s Ace programming language. The source code is available on GitHub and the type system is described in two award winning papers (see Publications). I also made some small contributions to Ace itself.

An OpenCL Type Checker

I wrote a type checker for v. 1.0.29 of the OpenCL specification in Python. My original plan was to use this library extend Ace with support for high-level GPU programming constructs, but I’ve since moved on to other projects. The source code is available on GitHub.

Formal Proofs

• A SCUBA dive computer (joint work with Viren Bajaj)
• An exploration of simple bifurcations
• Some simple examples of proving reachability properties using differential ghosts
• A model of a parachuter

Civics / Fun / Random

• A Perl framework for implementing and testing novel clustering algorithms.
• An alert system for Pittsburgh residents who want to avoid parking tickets.
• A tool for searching all Allegheny county dogs by name.
• A Scala library for pulling down Pittsburgh public transit information
• A static site geneartor for wedding image galleries
• A messaging service for debate tournaments
• A parser for MS Word files that use the Verbatim file format.