KnowledgeBase » SEMINAR » ID = 430

Verifying HORUS in Nuprl

by Jason Hickey
1995-1996

Abstract

ISIS and its successor, Horus, implement a collection of techniques for building software for disributed systems that performs well, is robust despite both hardware and software crashes, and exploits parallelism. ISIS has become very successful: hundreds of companies and Universities currently employ the toolkit in settings ranging from financial trading floors to telecommunications switching systems.

Recently we have undertaken an effort to show that the Horus system meets its specification. We plan to use Nuprl and formal techniques to verify key features of the Horus system ranging from fault tolerance guarantees to security.

In this seminar I will show our plans to incrementally "harden" the Horus system by constructing a reference implementation in ML and verifying it within a formal domain specifically designed for Horus. Work in the seminar is preliminary, and I will be concentrating on the formal component of the project in Nuprl.

This is joint work with Mark Hayden.