Do-Form: Motivation

This symposium is motivated by the long-term vision of making information systems dependable. In the past even mis-represented units of measurements caused fatal engineering disasters. In economics, the subtlety of issues involved in good auction design may have led to low revenues in auctions of public goods such as the 3G radio spectra. Similarly, banks' value-at-risk (VaR) models – the leading method of financial risk measurement – are too large and change too quickly to be thoroughly vetted by hand, the current state of the art; in the London Whale incident of 2012, JP Morgan claimed that its exposures were $67mn under one of its VaR models, and $129mn under another one. Verifying a model's properties requires formally specifying them; for VaR models, any work would have to start with this most basic step, as regulators' current desiderata are subjective and ambiguous. (For further background about economics, please see the ForMaRE project.)

We believe that these problems can be addressed by representing the knowledge underlying such models and mechanisms in a formal, explicit, machine-verifiable way. Contemporary computer science offers a wide choice of knowledge representation languages well supported by verification tools. Such tools have been successfully applied, e.g., for verifying software that controls commuter rail or payment systems. Still, domain experts without a strong computer science background find it challenging to choose the right tools and to use them. This symposium aims at investigating ways to support them. Some problems can be addressed now, others will bring new challenges to computer science.

This page was last modified on 10 April 2013.