Campus Event Calendar
Event Entry
What and Who
Formally Verified Data Structures Library for C. The String Data Structure
Artem Starostin
IMPRS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 10 July 2006
08:30
330 Minutes
E1 4
024
Saarbrücken
Abstract
Verisoft is a long-term research project whose main goal is the
formal verification of a complete computer system. The computer system ---
called the Academic system --- basically consists of hardware, an
operating system and user applications. User programs are written in a
high level programming language, a compiler for which is being verified in
the frame of the project. Together
with a compiler several libraries which implement basic data structures
and algorithms on them are provided. The talk gives an overview of the
formal framework and methods involded in the verification of such
libraries. The application of methods is illustrated by the data structure
for strings example.
formal verification of a complete computer system. The computer system ---
called the Academic system --- basically consists of hardware, an
operating system and user applications. User programs are written in a
high level programming language, a compiler for which is being verified in
the frame of the project. Together
with a compiler several libraries which implement basic data structures
and algorithms on them are provided. The talk gives an overview of the
formal framework and methods involded in the verification of such
libraries. The application of methods is illustrated by the data structure
for strings example.
Contact
Kerstin Kathy Meyer-Ross
226
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 06/26/2006 12:03 -- Created document.