Campus Event Calendar
Event Entry
What and Who
PhD Application Talk: Formal Verification of a Big Integer Library.
Sabine Fischer
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 29 October 2007
08:00
480 Minutes
E1 4
024
Saarbrücken
Abstract
I present formal correctness of a big integer library based on dynamically allocated lists. The package has been implemented in a programming language similar to C. In addition to the standard operations for big integers, the package provides a function which computes modulo exponentiation results using the square-and-multiply algorithm. We introduce predicates which help us deal with heap modification caused by function calls. Formal correctness has been verified with respect to partial correctness using the Hoare logic environment of the interactive theorem prover Isabelle.
Contact
IMPRS
225
--email hidden
passcode not visible
logged in users only
Lourdes Lara-Tapia, 10/26/2007 19:05 -- Created document.