|
|
(Apologies if you receive multiple copies of this announcement)
BCS-FACS Evening Seminar Series
Mechanising a correctness proof for a lock-free concurrent stack
Prof John Derrick (University of Sheffield)
21 September 2011
6pm
BCS London Offices
First Floor,
The Davidson Building
5 Southampton Street
London WC2E 7HA
http://www.bcs.org/upload/pdf/london-office-guide.pdf
In this talk we describe our recent work on developing refinement proofs
to show the correctness of concurrent implementations of data structures
such as the stack. The work involves developing proof obligations that
guarantee a form of refinement that in turn implies linearizability - the
correctness notion for such concurrent implementations.
Refreshments will be served from 5.30pm.
The seminar is free of charge and open to everyone. If you would
like to attend, please email Paul Boca [[log in to unmask]]
by >>> 20 September 2011<<<<
BCS-FACS Website: http://www.bcs-facs.org
Location of venue: http://www.bcs.org/upload/pdf/london-office-guide.pdf
|
|
|
|