Campus Event Calendar
Event Entry
What and Who
Formal Semantics of Remote Procedure Calls
Eyad Alkassar
Fachrichtung Informatik - Saarbrücken
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 6 July 2006
13:00
-- Not specified --
E1 3 - Hörsaal Gebäude
16
Saarbrücken
Abstract
The Verisoft project aims at the pervasive formal verification of entire
computer systems, from concrete hardware to the applications. Even
though literature and current research provide a large pool of theories
and tools for specifying and verifying programs, a theory capturing the
complete behaviour of e.g. a real operating system seemed not to be
seizable. However, formal -- i.e. computer aided and checked -- code
verification is getting more efficient and attractive even for
industrial use.
In my talk I will discuss some of the current hot topics in our project.
Formally proving correctness of an operating system kernel written in C0
includes building concurrent computation models and using an adequate
logic for program verification. We use a distributed extension of an
Hoare logics environment in Isabelle/HOL for that purpose. Furthermore I
will present the specification of a remote procedure call mechanism for
applications running concurrently in an operating system environment .
This mechanism establishes a simple to use client/server model and
illustrates how formalization of "real world" properties could be done
in the model stack.
computer systems, from concrete hardware to the applications. Even
though literature and current research provide a large pool of theories
and tools for specifying and verifying programs, a theory capturing the
complete behaviour of e.g. a real operating system seemed not to be
seizable. However, formal -- i.e. computer aided and checked -- code
verification is getting more efficient and attractive even for
industrial use.
In my talk I will discuss some of the current hot topics in our project.
Formally proving correctness of an operating system kernel written in C0
includes building concurrent computation models and using an adequate
logic for program verification. We use a distributed extension of an
Hoare logics environment in Isabelle/HOL for that purpose. Furthermore I
will present the specification of a remote procedure call mechanism for
applications running concurrently in an operating system environment .
This mechanism establishes a simple to use client/server model and
illustrates how formalization of "real world" properties could be done
in the model stack.
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 07/04/2006 15:10
Veronika Weinand, 04/26/2006 14:28
Veronika Weinand, 04/26/2006 14:21 -- Created document.
Veronika Weinand, 04/26/2006 14:28
Veronika Weinand, 04/26/2006 14:21 -- Created document.