-----------------------------------------------------------------------
TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar TDS Seminar
-----------------------------------------------------------------------

Title:  Verifying Snark: A Case Study in Formal Verification of a
Non-Blocking Algorithm that uses Dynamically Allocated Memory

Speaker: Simon Doherty

Place:   NE43-308
Time:    2:00pm - 3:30pm
Date:    Oct. 17, 2003

Abstract:

We describe an attempt to formally verify a non-blocking, dynamic-sized
double-ended queue (deque) implementation known as "Snark". This effort
revealed a bug in the algorithm; we describe a corrected version of the
algorithm and report on our experience in completing a correctness proof
for it.  Our verification models the deque algorithm and its specification
as IO Automata and uses the PVS system to encode the automata and prove
that the algorithm implements the specification.