Projects

AutoProof

During my PhD studies I was the main developer of AutoProof, an automated verifier for functional properties of Eiffel programs. AutoProof takes a contract-equipped Eiffel program and verifies that each function satisifes its postcondition whenever the precondition is satisfied. As an example of what AutoProof can do, take the following procedure of a clock class that increases the clock by one minute. It contains an obvious error on line 106, as it increases the number of minutes by 2 instead of 1.

increase_minutes
        -- Increase 'minutes' by one.
    note
        explicit: wrapping
    require
        modify_model (["minutes", "hours"], Current)
    do
        if minutes = 59 then
            set_minutes (0)
            increase_hours
        else
            set_minutes (minutes + 2)
        end
    ensure
        hours_set: old minutes = 59 implies hours = (old hours + 1) \\ 24
        hours_set: old minutes < 59 implies hours = old hours
        minutes_increased: minutes = (old minutes + 1) \\ 60
    end

The procedure contains a frame condition in the precondition - describing what the routine may modify - and a postcondition that describes the effect of the routine. Running AutoProof on the clock class that contains this procedure will result in the following output.

AutoProof Interface

AutoProof spots two errors. First, the call to set_minutes might fail as the function argument is restricted to the values between 0 and 59, but when the current value is 58 the call will fail. Second, the postcondition minutes_increased is violated as it states that the minutes attribute is only increased by 1. You can try it yourself (and fix the mentioned error).

AutoProof is available for download as part of the open-source Eiffel Verification Environment IDE or via an online interface. A list of example algorithms and programs that have been verified with AutoProof, for example sorting algorithms or a simple board game application, are available in an online repository.

Verification Assistant

The Verification Assistant is tool that automatically launches different verifiers and checkers in the background. A prototype, integrated in the Eiffel Verification Environment IDE, utilizes three different types of tools:

  • AutoProof: an automated verifier.
  • AutoTest: an automated testing tool based on random testing.
  • Eiffel Inspector: a light-weight static code checker.

The Verification Assistant takes care of launching the tools in the background and aggregates their results in a single display. This display uses a scoring system that combines the results of the various tools in a single correctness score which give the developer a broad overview of the state of the program.

Verification Assistant Interface

SeaBlast

During the ETH Master's course Game Programming Lab we have developed a submarine action game with a group of three people. The game features a 2D underwater playing field visualized using 3D graphics. A fluid-dynamics simulation is used to model underwater currents that influence the ships and weapons.

The game offers a campaign mode that can be played alone or cooperatively and a skirmish mode for up to four players. An AI takes on the role of the adversary in the campaign mode and can also substitute players in the skirmish mode.

My contribution to the project was the overall system architecture and development of the game engine, artificial intelligence, and user interface.

SeaBlast screenshot

Drupal Modules

For several years I was active in the Drupal community. I have developed several modules that help build a Wiki with Drupal:

  • The Wikitools module: Provides wiki behaviour for the Drupal website by handling requests to a specific area of the website. Nodes are identified by their name and links to inexistent nodes trigger a prompt to create a new node.
  • The Recent Changes module: List of recent changes including all subrevisions for the nodes. The module provides an RSS feed to easily follow the development of a website.
  • The Diff module: Reimplementation of the diff module to show differences between node revisions using the same diff-engine that MediaWiki uses.
  • The PEAR Wiki Filter module: Allows the use of various different wiki syntaxes as input filters.

Since I stopped developing Drupal modules a few years ago, all of these modules are now either maintained by other people or made obsolete.