Talk Title:
Reasoning about copyData: Yet Another Account of a Proof of
Correctness of an x86 Machine-Code Program

Shilpi Goel
19th October, 2015

Abstract:

I will describe in some detail my modus operandi for reasoning about a
new program using the x86isa books. The purpose of this talk is not to
present any novel technique but to illustrate the steps involved in
using the classical "clock functions" method to reason about an x86
machine-code program. If you would like to use the x86isa books to
reason about a program, either because you care about the program's
correctness or because you are looking for challenge problems in
program verification, this talk might help you get started.

I will use a copyData program as the illustrative example in this
talk.  This program copies data from a source array to a destination
array. Though the program itself is simple, its formal analysis is
interesting because it involves reasoning about loops and contiguous
memory locations (arrays).