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.
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.
|KeYmaera X website|
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.
- 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.