Languages:
Ada, C, Erlang, Java, MATLAB, OCaml, Prolog, Python, Swift
Frameworks and tools:
Web frameworks (Django, Pelican), formal-methods tools (SPIN, FDR, Otter, Isabelle, Coq, etc), LaTeX typesetting system, standard software-development tools (SVN/git, JUnit/OUnit/py.test, Make/Jenkins, profilers & debuggers, etc.)
Software:
Unfortunately, most of my software has been written for employers and so is not available for public download. I can, however, briefly describe my major projects here and can answer further questions about them by request.
- Customfit
- Webapp for knitters. Implemented in Django; build- and deploy-workflows managed by CircleCI, hosted by Heroku ans AWS. Supported 30K users.
- Knitter's Toolbox
- iOS app for knitters, implementing domain-specific calculators. Implemented in Swift. Purchased 2.3K+ times.
- Retreat Scheduler
- Finds near-optimal solutions to a sub-class of 'University scheduling problem'. Implemented as a thin wrapper around the PuLP family of LP modelers. I would not have even listed this program as a 'real' software project, but it allows me to make a point that I also made to my students: don't be scared of NP-completeness or asymptotic lower bounds. It is often the case (as it was here) that your actual needs can be met via approximation or by restricting your attention to more tractable sub-classes of the general problem. (Or, in this case, both.)
- Security and Privacy Assurance Research Test and Assessment (SPARTA) tool suite
- Stand-alone application for generating test-suites for databases. Written in Python. Produces synthetic (yet realistic) data, `interesting' queries over that data, and ground-truth answers for each query. Execution is unpredictable to database under test, but completely repeatable for experimental reproducibility. Parallelized and heavily optimized: runs 500X original speed; generates 120GB per core-hour.
- AES variant generator
- Generates secure random variants of the Advanced Encryption Standard in VHDL.
- Test framework for LibTomCrypt:
- Test framework, written in C, to test the correctness of cryptographic algorithms implemented as part of the LibTomCrypt library. Measured input and output of LibTomCrypt against test-vectors from standards-bodies and competing cryptographic library (OpenSSL). Written as part of larger evaluation of library for consulting project. Test-framework and resulting patches submitted back to LibTomCrypt developer.
- Experimental workbench for machine-learning:
- Experimental workbench, written in Erlang and Matlab, to support rapid experimentation and evaluation of machine-learning algorithms. Retrieved data from Erlang-based database, intelligently applied algorithms from the Matlab Statisical Toolbox. Evaluated algorithm-performance using standard measures from statistics (e.g., cross-validation). Enabled rapid development and selection of machine-learning algorithms for [REDACTED], supporting future core-business function of employer.
- The Cryptographic Protocol Programming Language (CPPL):
- A domain-speciļ¬c language for cryptographic protocols, with associated compiler, built on top of strand spaces and logical programming. Uses external libraries for automated reasoning (Datalog) and cryptographic operations (OpenSSL). Compiler implemented in OCaml. See accompanying paper, Programming Cryptographic Protocols, for language overview and (strand-based) semantics.
- The Cryptographic Protocol Shape Analyzer (CPSA):
- An automated analysis tool for security protocols. Efficiently explores possible protocol executions; automatically detects and reports possible attacks. (Distribution limited to government agencies and contractors.) Implemented in OCaml.
Standards
Use of static-static elliptic curve Diffie-Hellman key agreement in cryptographic message syntax. Jonathan Herzog and Roger Khazan. Request For Comments (RFC) 6278, June 2011.