Here is a summary of my major software projects.
XRT -- Exploring Runtime -- is an extensible exploration framework for programs represented in Microsoft's common intermediate language (CIL). Processing .NET managed assemblies, it provides means for analyzing, rewriting, and executing the rewritten program. One of XRT's extensions provides mixed concrete/symbolic exploration. Current major applications are in the area of testing, though XRT can be also used as software model-checker.
The XRT project was launched in fall 2004 and is ongoing work together with Nikolai Tillmann. On overview can be found here.
AsmL is an all-round modeling (specification) language for use in the Microsoft Environment. It incorporates concepts of Gurevich's Abstract State Machines, of specification languages like VDM or Z, of functional languages, and of modern object oriented languages. The language supports meta programming, allowing to explore non-determinism and dealing with state as first-class. It is embedded in .NET and compliant to the common language subset. AsmL comes with decent tool support. The language is bootstrapped, i.e. compiler and other tools are written in AsmL itself.
AsmL was implemented with significant contributions of Nikolai Tillmann and from others at FSE in the time span from fall 2001 to fall 2002.
In 2003, a different surface grammar was added to the AsmL system, oriented towards C#. The resulting language was first called A#, and later renamed to Spec#. The initial design and implementation of Spec# was done together with Robert Buessow.
ZETA is an open environment for the development of specification documents based on Z. It provides an integration framework for tools to edit, analyze and animate Z specifications and formalisms which are mapped to Z.
ZETA contains an execution engine for the Z notation which is based on techniques of concurrent constraint resolution and implements functional and logic computation features. This engine was explored in my PhD work.
ZETA was implemented with help of Robert Buessow and others in course of the research project ESPRESS from approx. fall 1998 to fall 1999. A white paper about the conceptual design can be found here.
Opal is a strongly typed, higher-order, strict, pure functional language. The objective of the Opal project, setup in around 1989, was to prove by experiment that declarative languages which incorporate features like value semantics and automatic memory management can be as efficiently executed than imperative languages like C. Today, Opal is one of the fastest pure functional language implementations around.
The Opal compilation system OCS and its supporting tools were written approx. in the time span from 1991 to 1993. The system is bootstrapped.