Category Archives: Global Financial System

Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?

Die Internationale Kelleruni Herrenbach veranstaltet im April eine öffentliche Vorlesung über Bitcoin und Blockchain.

Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?
Dr. Makarius Wenzel
Autor Christoph Ulrich Mayer
Freitag, 13. April 2018 um 19:30
Lebensraum Schwabencenter (“Wohnzimmer”)

Das “Wohnzimmer” im Schwabencenter ist ein umgenutztes Ladenlokal innerhalb des regulären Einkaufszentrums. Nach der Vorlesung gibt es noch etwas zu Essen.

Peter Biet von der Kelleruni schreibt hierzu:

Ich selber bin auf diese Vorlesung sehr gespannt, denn ich lese davon ständig in der Zeitung. Ich höre von vielen gerade jungen Menschen, die relativ große Summen in Bitcoins investieren und damit dann auch tatsächlich “richtig Kohle” machen. Ich höre von der Möglichkeit, Geldflüsse unabhängig von Banken zu inszenieren, aber auch von Schwarzgeldern, die da gewaschen werden. Ich höre außerdem von den riesigen Rechnerleistungen, die benötigt werden, um Bitcoins zu schürfen. Und vor allem weiß ich Eines: Ich verstehe das Ganze überhaupt nicht. Finde, obwohl ich versucht habe, mich zu informieren einfach keinen Zugang zu der Sache.
Vielleicht geht es manchen von euch ja genau so. Jedenfalls bin ich des Öfteren gebeten worden, dass wir uns mal dieses so aktuellen Themas annehmen sollten. Und so freue ich mich sehr und bin gewiss, dass Makarius und Christoph da etwas Licht in mein/unser Wissensdunkel bringen werden.

Hier das Material von Makarius.

Flattr this!

Grant Olney Passmore on Formal Verification of Financial Algorithms

On 25-Aug-2016, Grant Olney Passmore from Aesthetic Integration gave an invited talk at the ITP 2016 conference in Nancy, France. Here is the official announcement from the program:

Title: Formal Verification of Financial Algorithms, Progress and Prospects

Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we’ve pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we’ll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We’ll sketch many open problems and future directions along the way.

The session chair introduced the speaker as a colleague from the prover community who managed to get his private life covered by the NY Times.

Passmore then started his presentation with a promotional video, which is intended for people from the Financial Industry – without a background in formal logic or software verification. He pointed out that this is his first talk about the subject before an audience with expertise in theorem proving, and promised that many odd terms and buzzwords from the world of Finance would become clear later.

From his many slides, Passmore could fit only a small portion into the 60min time slot. A key point was the following Stack of Financial Algorithms (from top to bottom):

  • Collateral Trading
  • Inventory Management
  • Algo Containers
  • Trading Algorithms
  • Smart Order Routers
  • Venues

So far, Aesthetic Integration has mainly worked at the bottom: “Venues” are virtual places where trading happens, e.g. a “dark pool” as in the UBS Future of Finance Challenge (see also the white paper).

Passmore invited the prover community to participate in formal treatment of the whole stack given above. For example, full formalization of Financial Mathematics in Isabelle/HOL could support the slot “Trading Algorithms”.

He also presented the present flagship tool environment: Imandra. Here is a quotation from the official website:

What is Imandra?

AI’s Imandra is breakthrough artificial intelligence technology for ensuring financial algorithms are designed and implemented safely and fairly.

Powered by major recent advances in formal verification, Imandra:

  • Verifies correctness and stability of system designs for regulatory compliance
  • Uncovers nontrivial bugs
  • Tests – creates high-coverage test-suites
  • Saves – radically reduces associated costs

The system was demonstrated in two versions: one running on the local machine, and one running on a server (i.e. “in the cloud”). The interaction model is still mainly command-line based, but Aesthetics Integration is interested to improve on that.

Flattr this!