Software
This page describes my past and present open source academic software projects.
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 selfdriving cars, aircraft collision avoidance protocols, and surgical robots.
KeYmaera X website  GitHub repo  Online demo
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 bunch of course infrastructure for 15424, a course on verification of CyberPhysical Systems at CMU.
A Type System for String Analysis
I developed a type system that helps reduce errors in securitycritical 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 the Ave 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 highlevel 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.