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 self-driving 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

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

Civics / Fun / Random