Campus Event Calendar
Event Entry
What and Who
"Hot Topics in Verisoft"
Eyad Alkassar
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 26 October 2006
13:00
60 Minutes
E1 3 - Hörsaal Gebäude
016
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 for proving correctness of operatings system kernels one
needs to
argue about devices and their drivers. Hence a formal modeling of devices
throughout the model stack is requiered. We verified a simple harddisk
driver.
Finally on top of the OS, applications using Remote Procedure Calls can
be implemented.
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
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 for proving correctness of operatings system kernels one
needs to
argue about devices and their drivers. Hence a formal modeling of devices
throughout the model stack is requiered. We verified a simple harddisk
driver.
Finally on top of the OS, applications using Remote Procedure Calls can
be implemented.
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, 10/23/2006 15:06
Veronika Weinand, 10/19/2006 14:54
Veronika Weinand, 10/16/2006 17:07
Veronika Weinand, 10/16/2006 17:05 -- Created document.
Veronika Weinand, 10/19/2006 14:54
Veronika Weinand, 10/16/2006 17:07
Veronika Weinand, 10/16/2006 17:05 -- Created document.