Campus Event Calendar
Event Entry
What and Who
Verified Expression Evaluation for Multiplication and Division
Hristo Pentchev
IMPRS-CS
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, 26 February 2007
08:00
540 Minutes
E1 4
024
Saarbrücken
Abstract
The Verisoft project aims at the pervasive verification of an entire computer system including hardware, system software, compiler, and applications. The main programming language used in the Verisoft project is C0 (a dialect of C). This thesis reports on expression evaluation verification in the theorem prover Isabelle/HOL. The presented expression evaluation includes the operations multiplication, division, and modulo and is
specified in the scope of the formal C0 small step semantics. In this thesis we proved formally that the result of multiplication, division, and modulo in C0 is simulated by the code which is generated for these instructions by a simple C0 compiler (this compiler translates C0 programs to assembler code for the verified VAMP processor).
We conducted all formal proofs in Isabelle/HOL. This thesis presents a mathematical transcript of these formal proofs.
Contact
IMPRS
225
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 02/14/2007 09:57
Jennifer Gerling, 02/14/2007 09:39 -- Created document.
Jennifer Gerling, 02/14/2007 09:39 -- Created document.