Syllabus

The table below gives the planned syllabus for the seminar this semester. The syllabus lists the topics and papers to be discussed.

Material describing the course is available elsewhere.

Students should study the paper to be discussed prior to the meeting so that they can participate in the discussion.

This syllabus is provisional and subject to change. If it is necessary to revise the schedule, then this page will be updated to reflect the changes.

Date Paper or Topic Discussion Leader
Aug. 27 Plans for the semester Gary
Sep. 3 [Rodriguez-etal05]  
Sep. 10 (Internal draft to be given out in person, email Gary for a copy if you aren't at the seminar to receive one.) Deli
Sep. 17 No meeting.  
Sep. 24 [Herlihy-Shavit94] Christina
Oct. 1 [Owicki-Gries76] Gary
Oct. 8 (Internal draft sent to you in email.) Carlos
Oct. 15 [Jones96] Yuyan
Oct. 22 No seminar (SPLASH conference)  
Oct. 29 [Herlihy93] Carlos
Nov. 5 [Morris89] Jose
Nov. 12 [Hoare72] Gary
Nov. 19 [Norris-Demsky13] Damian
Nov. 26 [Burckhardt-etal10] Christina

Bibliography

Note that you can use each paper's DOI link to get a copy of it, when you are on the UCF network.

[Burckhardt-etal10]
Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. Line-up: A complete and automatic linearizability checker. In PLDI'10 Proceedings of the 2010 ACM SIGPLAN conference on Programming Language Design and Implementation, pages 330-340, Toronto, Canada, ACM, 2010. http://dx.doi.org/10.1145/1806596.1806634
[Herlihy-Shavit94]
Maurice Herlihy and Nir Shavit. A Simple Constructive Computability Theorem for Wait-free Computation. In STOC '94 Proceedings of the twenty-sixth annual ACM Symposium on Theory of Computing, pages 243-252, Montreal, Canada, ACM, 1994. http://dx.doi.org/10.1145/195058.195144
[Herlihy93]
Maurice Herlihy. A methodology for implementing highly concurrent data objects. ACM Transactions on Programming Languages and Systems, 15(5):745-770, November, 1993. http://dx.doi.org/10.1145/161468.161469
[Hoare72]
C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271-281, 1972. http://dx.doi.org/10.1007/BF00289507
[Jones96]
Cliff B. Jones. Accommodating Interference in the Formal Design of Concurrent Object-Based Programs. Formal Methods in System Design 8(2):105-122, March, 1996. ttp://dx.doi.org/10.1007/BF00122417
[Morris89]
Joseph M. Morris. Laws of Data Refinement. Acta Informatica 26(4):287-308, February 1989. http://dx.doi.org/10.1007/BF00276019
[Norris-Demsky13]
Brian Norris and Brian Demsky. CDSCHECKER: Checking Concurrent Data Structures Written with C/C++ Atomics. In OOPSLA'13, Indianapolis, IN, pp. 131-150, ACM, 2013. http://dx.doi.org/10.1145/2509136.2509514
[Owicki-Gries76]
Susan Owicki and David Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM 19(5):279-285, May 1976. http://dx.doi.org/10.1145/360051.360224
[Rodriguez-etal05]
Edwin Rodriguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, and Robby. Extending JML for Modular Specification and Verification of Multi-Threaded Programs. In Andrew P. Black (ed.), ECOOP 2005 --- Object-Oriented Programming 19th European Conference, Glasgow, UK, pp. 551-576, Springer-Verlag, 2005. Lecture Notes in Computer Science, volume 3586, http://dx.doi.org/10.1007/11531142_24

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

Last modified Thursday, November 20, 2014.