Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
From Program Verification to Certified Binaries

Edit abstract data

Author(s): Angelos Manousaridis, Michalis Papakyriakou and Nikolaos Papaspyrou
Slot: Wed, 17:50-18:10, Room 22 (col. 4)

Abstract

The long tradition of formal program verification and
the more recent frameworks for proof-carrying code
share a common goal: the construction of certified software.
In this paper, mainly through a simple motivating example,
we describe our vision of a complete hybrid system
that combines the two approaches,
We discuss the feasibility of such an ambitious project
and report on progress made so far.

websites: Arnold Beckmann 2008-05-19 Valid HTML 4.01! Valid CSS!