Since August 2007 I've been teaching computer science at Messiah College, in Grantham, PA. This fall I am teaching Computer Programming I (COSC 181), Computer Programming II (COSC 182), and System Internals and Assembly Language (COSC 281). These are all accessible via moodle.messiah.edu (guest access is enabled for all three courses).

From January 2000 to June 2007 I did software verification research at the NASA IV&V Facility in Fairmont, WV, working part-time for ProLogic, Inc. and as a graduate student in the computer science department at West Virginia University, under Tim Menzies and Bojan Cukic. The papers listed and research described below began with their ideas about practical ways to apply random search to software verification.

Model checkers (SPIN and SMV are two of the most popular) are software tools used to formally verify that a system of finite-state machines satisfies (is a model of) a set of temporal logic properties. In general this task requires an exponential amount of memory (i.e., too much), compared to the size of the input, so model checkers are only used to check relatively small systems (or relatively small abstractions of larger systems). Lurch is a debugging tool for models of finite-state concurrent systems, an alternative to model checking based on a simple random search procedure. Like a model checker, Lurch detects faults and for each fault detected produces a trace file showing a path from initial conditions to the fault. Unlike a model checker, Lurch uses very little memory by sampling (rather than performing a complete exploration of) the state space.

A couple years ago I started working on a big project: to write a series of songs from the text of the Gospel of Mark. Here are a few of the songs I like best from what I've been able to write and record so far: