Downloadable software

Over the years, I have authored and contributed to a number of free software projects, some of which originate from research projects.

Open source and system utilities

  • GCC - The GNU Compiler Collection
    I contributed to the GNU Compiler Collection which offers optimised code generation for a large number of different hard and software platforms. I have picked up and contributed work mainly to do with tail call optimisation, which ended up in version 3.4 of GCC.

  • Mailfilter - An anti-spam utility
    Mailfilter is a flexible utility for UNIX (-like) operating systems to get rid of unwanted SPAM mails, before having to go through the trouble of downloading them into the local computer. It offers support for one or many POP accounts and is especially useful for dialup connections via modem, ISDN, etc. If you're running a more or less standard Linux or BSD distribution, chances are that Mailfilter is already preconfigured and packaged for you.

  • Nazghul - A roleplaying game similar to Ultima 5
    Recently, I'm reliving glorious memories of my childhood by contributing a wee bit of GNU-tools wizardry to the wonderful project Nazghul. Nazghul is a computer roleplaying game similar in style to Ultima 4 and 5. Great programmers, great game, so please check it out!

Software supporting mostly academic research

  • ABsolver - Arithmetic-Boolean Constraint Solver
    ABsolver is a system library and stand-alone program for solving mixed-domain, i.e., (non-linear) arithmetic-boolean constraints. It provides a common interface for various constraint and SAT-solvers.

  • Beagle - Theorem Prover for Hierarchic Superposition with Weak Abstraction
    Beagle is an automated theorem prover for first-order logic with equality over linear integer arithmetic. It accepts formulas in the FOF, TFF, and TFF-INT formats of the TPTP syntax.
    My contribution are solvers for linear arithmetic.

  • G12 - Constraint Programming Platform and IDE
    A software platform for solving large scale industrial combinatorial optimisation problems. I worked on the G12IDE, which allows an on-the-fly debugging and custom visualisation of constraint problems using a built-in scripting language.

  • LTL3 Tools - A tool set to generate LTL monitors New!
    The LTL3 tools are a collection of programs that convert a given LTL formula into a finite-state machine, which can be used as a monitor for that formula. Basically, this is a tool for runtime verification.

  • SALT - Structured Assertion Language for Temporal Logic
    SALT is a general purpose, programming-language-like assertion and specification language for temporal logic. As such it includes specification techniques for both untimed and timed reactive systems, a compiler, and a web front-end. (The industrial counterpart, so to speak, is IEEE1850, PSL.)

Minor code snippets and abandoned projects

You might also like to look at my code snippets for lots of useful little bits of software that I have written over the years.