Failboxes

(formerly known as subsystems)

Bart Jacobs and Frank Piessens

We are investigating programming constructs for making it easier to deliver programs that provably preserve the program's intended safety properties in the presence of unchecked exceptions (including exceptions caused by internal problems in the virtual machine, which may occur at any program point). This web page is about work done on one such mechanism, which we call failboxes.

Paper:

Bart Jacobs and Frank Piessens. Failboxes: Provably Safe Exception Handling. ECOOP 2009. [slides]

The source code for an implementation in C# 3.0, for the .NET Framework:

Subsystems.cs
PerfTests.cs

The source code for an implementation in Scala, for the Java Platform:

subsystems.scala
testsuite.scala

Machine-checked metatheory, using the Coq proof assistant: metatheory.

Program verifier prototype: exceptflat.

Last update: 2009-07-13.