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

Amazon CodeWhisperer

CodeWhisperer is an AI code generator developed by a large team at AWS (of which I was a member). One of Amazon’s first AI products to enter General Availability, CodeWhisperer was highlighted in two letters to shareholders as proof of Amazon’s leadership in the AI space.

IBM 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.

KeYmaera X website
GitHub repo

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

Civics / Fun / Random