dissertation.bib

@InCollection{sep-logic-substructural,
	author       =	{Restall, Greg},
	title        =	{Substructural Logics},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{http://plato.stanford.edu/archives/sum2009/entries/logic-substructural/}},
	year         =	{2009},
	edition      =	{Summer 2009},
}

@inproceedings{DBLP:conf/mfcs/Wadler93,
  author    = {Philip Wadler},
  title     = {A Taste of Linear Logic},
  booktitle = {MFCS},
  year      = {1993},
  pages     = {185-210},
  ee        = {http://dx.doi.org/10.1007/3-540-57182-5_12},
  crossref  = {DBLP:conf/mfcs/1993},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/mfcs/1993,
  editor    = {Andrzej M. Borzyszkowski and
               Stefan Sokolowski},
  title     = {Mathematical Foundations of Computer Science 1993, 18th
               International Symposium, MFCS'93, Gdansk, Poland, August
               30 - September 3, 1993, Proceedings},
  booktitle = {MFCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {711},
  year      = {1993},
  isbn      = {3-540-57182-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/popl/SarkarSNORBMA09,
  author    = {Susmit Sarkar and
               Peter Sewell and
               Francesco Zappa Nardelli and
               Scott Owens and
               Tom Ridge and
               Thomas Braibant and
               Magnus O. Myreen and
               Jade Alglave},
  title     = {The semantics of {x86-CC} multiprocessor machine code},
  booktitle = {POPL},
  year      = {2009},
  pages     = {379-391},
  ee        = {http://doi.acm.org/10.1145/1480881.1480929},
  crossref  = {DBLP:conf/popl/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2009,
  editor    = {Zhong Shao and
               Benjamin C. Pierce},
  title     = {Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2009, Savannah,
               GA, USA, January 21-23, 2009},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2009},
  isbn      = {978-1-60558-379-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/tphol/OwensSS09,
  author    = {Scott Owens and
               Susmit Sarkar and
               Peter Sewell},
  title     = {A Better x86 Memory Model: x86-{TSO}},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {391-407},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03359-9_27},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tphol/2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International
               Conference, TPHOLs 2009, Munich, Germany, August 17-20,
               2009. Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  year      = {2009},
  isbn      = {978-3-642-03358-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03359-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@inproceedings{DBLP:conf/popl/AlglaveFIMSSN09,
  author    = {Jade Alglave and
               Anthony C. J. Fox and
               Samin Ishtiaq and
               Magnus O. Myreen and
               Susmit Sarkar and
               Peter Sewell and
               Francesco Zappa Nardelli},
  title     = {The semantics of {Power} and {ARM} multiprocessor machine code},
  booktitle = {DAMP},
  year      = {2009},
  pages     = {13-24},
  ee        = {http://doi.acm.org/10.1145/1481839.1481842},
  crossref  = {DBLP:conf/popl/2009damp},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2009damp,
  editor    = {Leaf Petersen and
               Manuel M. T. Chakravarty},
  title     = {Proceedings of the POPL 2009 Workshop on Declarative Aspects
               of Multicore Programming, DAMP 2009, Savannah, GA, USA,
               January 20, 2009},
  booktitle = {DAMP},
  publisher = {ACM},
  year      = {2009},
  isbn      = {978-1-60558-417-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/BoudolP09,
  author    = {G{\'e}rard Boudol and
               Gustavo Petri},
  title     = {Relaxed memory models: an operational approach},
  booktitle = {POPL},
  year      = {2009},
  pages     = {392-403},
  ee        = {http://doi.acm.org/10.1145/1480881.1480930},
  crossref  = {DBLP:conf/popl/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/concur/Brookes04,
  author    = {Stephen D. Brookes},
  title     = {A Semantics for Concurrent Separation Logic},
  booktitle = {CONCUR},
  year      = {2004},
  pages     = {16-34},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3170{\&}spage=16},
  crossref  = {DBLP:conf/concur/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/concur/2004,
  editor    = {Philippa Gardner and
               Nobuko Yoshida},
  title     = {CONCUR 2004 - Concurrency Theory, 15th International Conference,
               London, UK, August 31 - September 3, 2004, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3170},
  year      = {2004},
  isbn      = {3-540-22940-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tcs/OHearn07,
  author    = {Peter W. O'Hearn},
  title     = {Resources, concurrency, and local reasoning},
  journal   = {Theor. Comput. Sci.},
  volume    = {375},
  number    = {1-3},
  year      = {2007},
  pages     = {271-307},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.12.035},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/tc/Lamport79,
  author    = {Leslie Lamport},
  title     = {How to Make a Multiprocessor Computer That Correctly Executes
               Multiprocess Programs},
  journal   = {IEEE Trans. Computers},
  volume    = {28},
  number    = {9},
  year      = {1979},
  pages     = {690-691},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/concur/HoareMSW09,
  author    = {C. A. R. Hoare and
               Bernhard M{\"o}ller and
               Georg Struth and
               Ian Wehrman},
  title     = {Concurrent {Kleene} Algebra},
  booktitle = {CONCUR},
  year      = {2009},
  pages     = {399-414},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04081-8_27},
  crossref  = {DBLP:conf/concur/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/concur/2009,
  editor    = {Mario Bravetti and
               Gianluigi Zavattaro},
  title     = {CONCUR 2009 - Concurrency Theory, 20th International Conference,
               CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5710},
  year      = {2009},
  isbn      = {978-3-642-04080-1},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04081-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@incollection{graphicalmodelsMarktoberdorf,
  author    = {C. A. R. Hoare and Ian Wehrman and Peter W. O'Hearn},
  title     = {Graphical Models of Separation Logic},
  booktitle = {Engineering Methods and Tools for Software Safety and
                  Security},
  editor    = {M. Broy and D. Harel and C. A. R. Hoare},
  publisher = {IOS Press},
  year      = {2009},
  note      = {To appear}
}

@article{DBLP:journals/tcs/WehrmanKCM08,
  author    = {Ian Wehrman and
               David Kitchin and
               William R. Cook and
               Jayadev Misra},
  title     = {A timed semantics of Orc},
  journal   = {Theor. Comput. Sci.},
  volume    = {402},
  number    = {2-3},
  year      = {2008},
  pages     = {234-248},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2008.04.037},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{tcs07-tr,
  author =       "Ian Wehrman and David Kitchin and William R. Cook and Jayadev Misra",
  title =        "{Properties of the Timed Operational and Denotational Semantics of Orc}",
  institution =  "University of Texas at Austin, Department of Computer Sciences",
  year =         2007,
  number =       "TR-07-65",
}

@article{SteinkeNutt,
 author = {Steinke,, Robert C. and Nutt,, Gary J.},
 title = {A unified theory of shared memory consistency},
 journal = {J. ACM},
 volume = {51},
 number = {5},
 year = {2004},
 issn = {0004-5411},
 pages = {800--849},
 doi = {http://doi.acm.org/10.1145/1017460.1017464},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@techreport{higham98weak,
  author = "L. Higham and J. Kawash and N. Verwaal",
  title = "Weak Memory Consistency Models Part {I}: Definitions and Comparisons",
  number = "98/612/03",
  institution = "Department of Computer Science, The University of Calgary ",
  year = "1998",
  url = "citeseer.ist.psu.edu/higham98weak.html" 
}


@PHDTHESIS{JonesRelyGuar,
AUTHOR = "Cliff B. Jones",
TITLE = "Development methods for computer programs including a notion of interference",
SCHOOL = "Oxford University",
YEAR = "1981"}

@article{DBLP:journals/fac/XuRH97,
  author    = {Qiwen Xu and
               Willem P. de Roever and
               Jifeng He},
  title     = {The Rely-Guarantee Method for Verifying Shared Variable
               Concurrent Programs},
  journal   = {Formal Asp. Comput.},
  volume    = {9},
  number    = {2},
  year      = {1997},
  pages     = {149-174},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/bsl/OHearnP99,
  author    = {Peter W. O'Hearn and
               David J. Pym},
  title     = {The logic of bunched implications},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {5},
  number    = {2},
  year      = {1999},
  pages     = {215-244},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0502/0502-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tcs/PymOY04,
  author    = {David J. Pym and
               Peter W. O'Hearn and
               Hongseok Yang},
  title     = {Possible worlds and resources: the semantics of {BI}},
  journal   = {Theor. Comput. Sci.},
  volume    = {315},
  number    = {1},
  year      = {2004},
  pages     = {257-305},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2003.11.020},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/IshtiaqO01,
  author    = {Samin S. Ishtiaq and
               Peter W. O'Hearn},
  title     = {{BI} as an Assertion Language for Mutable Data Structures},
  booktitle = {POPL},
  year      = {2001},
  pages     = {14-26},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lics/Reynolds02,
  author    = {John C. Reynolds},
  title     = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {LICS},
  year      = {2002},
  pages     = {55-74},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029817},
  crossref  = {DBLP:conf/lics/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/lics/2002,
  title     = {17th IEEE Symposium on Logic in Computer Science (LICS 2002),
               22-25 July 2002, Copenhagen, Denmark, Proceedings},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year      = {2002},
  isbn      = {0-7695-1483-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/csl/OHearnRY01,
  author    = {Peter W. O'Hearn and
               John C. Reynolds and
               Hongseok Yang},
  title     = {Local Reasoning about Programs that Alter Data Structures},
  booktitle = {CSL},
  year      = {2001},
  pages     = {1-19},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2142/21420001.htm},
  crossref  = {DBLP:conf/csl/2001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/csl/2001,
  editor    = {Laurent Fribourg},
  title     = {Computer Science Logic, 15th International Workshop, CSL
               2001. 10th Annual Conference of the EACSL, Paris, France,
               September 10-13, 2001, Proceedings},
  booktitle = {CSL},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2142},
  year      = {2001},
  isbn      = {3-540-42554-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/concur/VafeiadisP07,
  author    = {Viktor Vafeiadis and
               Matthew J. Parkinson},
  title     = {A Marriage of Rely/Guarantee and Separation Logic},
  booktitle = {CONCUR},
  year      = {2007},
  pages     = {256-271},
  ee        = {http://dx.doi.org/10.1007/978-3-540-74407-8_18},
  crossref  = {DBLP:conf/concur/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/concur/2007,
  editor    = {Lu\'{\i}s Caires and
               Vasco Thudichum Vasconcelos},
  title     = {CONCUR 2007 - Concurrency Theory, 18th International Conference,
               CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4703},
  year      = {2007},
  isbn      = {978-3-540-74406-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/sas/CalcagnoPV07,
  author    = {Cristiano Calcagno and
               Matthew J. Parkinson and
               Viktor Vafeiadis},
  title     = {Modular Safety Checking for Fine-Grained Concurrency},
  booktitle = {SAS},
  year      = {2007},
  pages     = {233-248},
  ee        = {http://dx.doi.org/10.1007/978-3-540-74061-2_15},
  crossref  = {DBLP:conf/sas/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/sas/2007,
  editor    = {Hanne Riis Nielson and
               Gilberto Fil{\'e}},
  title     = {Static Analysis, 14th International Symposium, SAS 2007,
               Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings},
  booktitle = {SAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4634},
  year      = {2007},
  isbn      = {978-3-540-74060-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/aplas/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Symbolic Execution with Separation Logic},
  booktitle = {APLAS},
  year      = {2005},
  pages     = {52-68},
  ee        = {http://dx.doi.org/10.1007/11575467_5},
  crossref  = {DBLP:conf/aplas/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aplas/2005,
  editor    = {Kwangkeun Yi},
  title     = {Programming Languages and Systems, Third Asian Symposium,
               APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings},
  booktitle = {APLAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3780},
  year      = {2005},
  isbn      = {3-540-29735-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/fmco/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Smallfoot: Modular Automatic Assertion Checking with Separation
               Logic},
  booktitle = {FMCO},
  year      = {2005},
  pages     = {115-137},
  ee        = {http://dx.doi.org/10.1007/11804192_6},
  crossref  = {DBLP:conf/fmco/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/fmco/2005,
  editor    = {Frank S. de Boer and
               Marcello M. Bonsangue and
               Susanne Graf and
               Willem P. de Roever},
  title     = {Formal Methods for Components and Objects, 4th International
               Symposium, FMCO 2005, Amsterdam, The Netherlands, November
               1-4, 2005, Revised Lectures},
  booktitle = {FMCO},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4111},
  year      = {2006},
  isbn      = {3-540-36749-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lics/CalcagnoOY07,
  author    = {Cristiano Calcagno and
               Peter W. O'Hearn and
               Hongseok Yang},
  title     = {Local Action and Abstract Separation Logic},
  booktitle = {LICS},
  year      = {2007},
  pages     = {366-378},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/LICS.2007.30},
  crossref  = {DBLP:conf/lics/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/lics/2007,
  title     = {22nd IEEE Symposium on Logic in Computer Science (LICS 2007),
               10-12 July 2007, Wroclaw, Poland, Proceedings},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/cacm/Hoare69,
  author    = {C. A. R. Hoare},
  title     = {An Axiomatic Basis for Computer Programming},
  journal   = {Commun. ACM},
  volume    = {12},
  number    = {10},
  year      = {1969},
  pages     = {576-580},
  ee        = {http://doi.acm.org/10.1145/363235.363259},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/toplas/HerlihyW90,
  author    = {Maurice Herlihy and
               Jeannette M. Wing},
  title     = {Linearizability: A Correctness Condition for Concurrent
               Objects},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {12},
  number    = {3},
  year      = {1990},
  pages     = {463-492},
  ee        = {http://doi.acm.org/10.1145/78969.78972},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/GotsmanCPV09,
  author    = {Alexey Gotsman and
               Byron Cook and
               Matthew J. Parkinson and
               Viktor Vafeiadis},
  title     = {Proving that non-blocking algorithms don't block},
  booktitle = {POPL},
  year      = {2009},
  pages     = {16-28},
  ee        = {http://doi.acm.org/10.1145/1480881.1480886},
  crossref  = {DBLP:conf/popl/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@misc{treiber:stack86,
	author = {R.K.Treiber},
	title = {Systems Programming: Coping with Parallelism. RJ5118},
	year = 1986,
	month = {April},
	institution = {IBM Almaden Research Center}}


@inproceedings{DBLP:conf/podc/MichaelS96,
  author    = {Maged M. Michael and
               Michael L. Scott},
  title     = {Simple, Fast, and Practical Non-Blocking and Blocking Concurrent
               Queue Algorithms},
  booktitle = {PODC},
  year      = {1996},
  pages     = {267-275},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/CalcagnoGZ05,
  author    = {Cristiano Calcagno and
               Philippa Gardner and
               Uri Zarfaty},
  title     = {Context logic and tree update},
  booktitle = {POPL},
  year      = {2005},
  pages     = {271-282},
  ee        = {http://doi.acm.org/10.1145/1040305.1040328},
  crossref  = {DBLP:conf/popl/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2005,
  editor    = {Jens Palsberg and
               Mart\'{\i}n Abadi},
  title     = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2005, Long Beach,
               California, USA, January 12-14, 2005},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2005},
  isbn      = {1-58113-830-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/entcs/CalcagnoGZ07,
  author    = {Cristiano Calcagno and
               Philippa Gardner and
               Uri Zarfaty},
  title     = {Local Reasoning about Data Update},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {172},
  year      = {2007},
  pages     = {133-175},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2007.02.006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tphol/Ridge07,
  author    = {Tom Ridge},
  title     = {Operational Reasoning for Concurrent Caml Programs and Weak
               Memory Models},
  booktitle = {TPHOLs},
  year      = {2007},
  pages     = {278-293},
  ee        = {http://dx.doi.org/10.1007/978-3-540-74591-4_21},
  crossref  = {DBLP:conf/tphol/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tphol/2007,
  editor    = {Klaus Schneider and
               Jens Brandt},
  title     = {Theorem Proving in Higher Order Logics, 20th International
               Conference, TPHOLs 2007, Kaiserslautern, Germany, September
               10-13, 2007, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4732},
  year      = {2007},
  isbn      = {978-3-540-74590-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/GuerraouiHS09,
  author    = {Rachid Guerraoui and
               Thomas A. Henzinger and
               Vasu Singh},
  title     = {Software Transactional Memory on Relaxed Memory Models},
  booktitle = {CAV},
  year      = {2009},
  pages     = {321-336},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02658-4_26},
  crossref  = {DBLP:conf/cav/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2009,
  editor    = {Ahmed Bouajjani and
               Oded Maler},
  title     = {Computer Aided Verification, 21st International Conference,
               CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5643},
  year      = {2009},
  isbn      = {978-3-642-02657-7},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02658-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/ipl/WehrmanHO09,
  author    = {Ian Wehrman and
               C. A. R. Hoare and
               Peter W. O'Hearn},
  title     = {Graphical models of separation logic},
  journal   = {Inf. Process. Lett.},
  volume    = {109},
  number    = {17},
  year      = {2009},
  pages     = {1001-1004},
  ee        = {http://dx.doi.org/10.1016/j.ipl.2009.06.003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/cacm/OwickiG76,
  author    = {Susan S. Owicki and
               David Gries},
  title     = {Verifying Properties of Parallel Programs: An Axiomatic
               Approach},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {5},
  year      = {1976},
  pages     = {279-285},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/acta/OwickiG76,
  author    = {Susan S. Owicki and
               David Gries},
  title     = {An Axiomatic Proof Technique for Parallel Programs I},
  journal   = {Acta Inf.},
  volume    = {6},
  year      = {1976},
  pages     = {319-340},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/pods/GardnerSWZ08,
  author    = {Philippa Gardner and
               Gareth Smith and
               Mark J. Wheelhouse and
               Uri Zarfaty},
  title     = {Local Hoare reasoning about DOM},
  booktitle = {PODS},
  year      = {2008},
  pages     = {261-270},
  ee        = {http://doi.acm.org/10.1145/1376916.1376953},
  crossref  = {DBLP:conf/pods/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/pods/2008,
  editor    = {Maurizio Lenzerini and
               Domenico Lembo},
  title     = {Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART
               Symposium on Principles of Database Systems, PODS 2008,
               June 9-11, 2008, Vancouver, BC, Canada},
  booktitle = {PODS},
  publisher = {ACM},
  year      = {2008},
  isbn      = {978-1-60558-108-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tse/KaufmannM97,
  author    = {Matt Kaufmann and
               J. Strother Moore},
  title     = {An Industrial Strength Theorem Prover for a Logic Based
               on Common Lisp},
  journal   = {IEEE Trans. Software Eng.},
  volume    = {23},
  number    = {4},
  year      = {1997},
  pages     = {203-213},
  ee        = {http://www.computer.org/tse/ts1997/e0203abs.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DBLP:books/sp/NipkowPW02,
  author    = {Tobias Nipkow and
               Lawrence C. Paulson and
               Markus Wenzel},
  title     = {Isabelle/HOL - A Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2283},
  year      = {2002},
  isbn      = {3-540-43376-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{CoqBook,
  author       = "Bertot, Yves and Cast\'eran, Pierre",
  title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
  series       = "Texts in Theoretical Computer Science",
  year         = "2004",
  publisher    = "Springer Verlag",
  url          = "http://www.labri.fr/publications/l3a/2004/BC04"
}

@inproceedings{DBLP:conf/cc/BurckhardtMS10,
  author    = {Sebastian Burckhardt and
               Madanlal Musuvathi and
               Vasu Singh},
  title     = {Verifying Local Transformations on Relaxed Memory Models},
  booktitle = {CC},
  year      = {2010},
  pages     = {104-123},
  ee        = {http://dx.doi.org/10.1007/978-3-642-11970-5_7},
  crossref  = {DBLP:conf/cc/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cc/2010,
  editor    = {Rajiv Gupta},
  title     = {Compiler Construction, 19th International Conference, CC
               2010, Held as Part of the Joint European Conferences on
               Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus,
               March 20-28, 2010. Proceedings},
  booktitle = {CC},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6011},
  year      = {2010},
  isbn      = {978-3-642-11969-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-11970-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/AtigBBM10,
  author    = {Mohamed Faouzi Atig and
               Ahmed Bouajjani and
               Sebastian Burckhardt and
               Madanlal Musuvathi},
  title     = {On the verification problem for weak memory models},
  booktitle = {POPL},
  year      = {2010},
  pages     = {7-18},
  ee        = {http://doi.acm.org/10.1145/1706299.1706303},
  crossref  = {DBLP:conf/popl/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2010,
  editor    = {Manuel V. Hermenegildo and
               Jens Palsberg},
  title     = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2010, Madrid,
               Spain, January 17-23, 2010},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-60558-479-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/esop/FerreiraFS10,
  author    = {Rodrigo Ferreira and
               Xinyu Feng and
               Zhong Shao},
  title     = {Parameterized Memory Models and Concurrent Separation Logic},
  booktitle = {ESOP},
  year      = {2010},
  pages     = {267-286},
  ee        = {http://dx.doi.org/10.1007/978-3-642-11957-6_15},
  crossref  = {DBLP:conf/esop/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/esop/2010,
  editor    = {Andrew D. Gordon},
  title     = {Programming Languages and Systems, 19th European Symposium
               on Programming, ESOP 2010, Held as Part of the Joint European
               Conferences on Theory and Practice of Software, ETAPS 2010,
               Paphos, Cyprus, March 20-28, 2010. Proceedings},
  booktitle = {ESOP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6012},
  year      = {2010},
  isbn      = {978-3-642-11956-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-11957-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TECHREPORT{VafeiadisDissertation,
    author = {Viktor Vafeiadis},
    title = {Modular fine-grained concurrency verification},
    institution = {University of Cambridge},
    year = {2008},
    note = {Technical Report UCAM-CL-TR-726}
}

@inproceedings{DBLP:conf/cav/YangLBCCDO08,
  author    = {Hongseok Yang and
               Oukseh Lee and
               Josh Berdine and
               Cristiano Calcagno and
               Byron Cook and
               Dino Distefano and
               Peter W. O'Hearn},
  title     = {Scalable Shape Analysis for Systems Code},
  booktitle = {CAV},
  year      = {2008},
  pages     = {385-398},
  ee        = {http://dx.doi.org/10.1007/978-3-540-70545-1_36},
  crossref  = {DBLP:conf/cav/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2008,
  editor    = {Aarti Gupta and
               Sharad Malik},
  title     = {Computer Aided Verification, 20th International Conference,
               CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5123},
  year      = {2008},
  isbn      = {978-3-540-70543-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@phdthesis{Yang-thesis,
   AUTHOR= {Hongseok Yang},
   TITLE= {Local Reasoning for Stateful Programs},
   YEAR= {2001},
   SCHOOL= {University of Illinois at Urbana-Champaign},
   NOTE= {Technical Report UIUCDCS-R-2001-2227},
}

@inproceedings{DBLP:conf/asplos/ChongI08,
  author    = {Nathan Chong and
               Samin Ishtiaq},
  title     = {{Reasoning about the ARM weakly consistent memory model}},
  booktitle = {MSPC},
  year      = {2008},
  pages     = {16-19},
  ee        = {http://doi.acm.org/10.1145/1353522.1353528},
  crossref  = {DBLP:conf/asplos/2008mspc},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/asplos/2008mspc,
  editor    = {Emery D. Berger and
               Brad Chen},
  title     = {Proceedings of the 2008 ACM SIGPLAN workshop on Memory Systems
               Performance and Correctness: held in conjunction with the
               Thirteenth International Conference on Architectural Support
               for Programming Languages and Operating Systems (ASPLOS
               '08), Seattle, Washington, USA, March 2, 2008},
  booktitle = {MSPC},
  publisher = {ACM},
  year      = {2008},
  isbn      = {978-1-60558-049-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{wmsldetails,
  author =       "Ian Wehrman",
  title =        "Semantics and Syntax of a Weak-Memory Concurrent Separation Logic: Sequential Fragment",
  institution =  "University of Texas at Austin, Department of Computer Science",
  year =         2010,
  number =       "TR-12-08",
}

@inproceedings{DBLP:conf/spaa/HendlerSY04,
  author    = {Danny Hendler and
               Nir Shavit and
               Lena Yerushalmi},
  title     = {A scalable lock-free stack algorithm},
  booktitle = {SPAA},
  year      = {2004},
  pages     = {206-215},
  ee        = {http://doi.acm.org/10.1145/1007912.1007944},
  crossref  = {DBLP:conf/spaa/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/spaa/2004,
  editor    = {Phillip B. Gibbons and
               Micah Adler},
  title     = {SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium
               on Parallel Algorithms, June 27-30, 2004, Barcelona, Spain},
  booktitle = {SPAA},
  publisher = {ACM},
  year      = {2004},
  isbn      = {1-58113-840-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{model-checking,
 author = {Clarke, Edmund M. and Emerson, E. Allen},
 title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic},
 booktitle = {Logic of Programs, Workshop},
 year = {1982},
 isbn = {3-540-11212-X},
 pages = {52--71},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@book{unity-book,
 author = {Chandy, K. Mani and Misra, Jayadev},
 title = {Parallel program design: a foundation},
 year = {1988},
 isbn = {0-201-05866-9},
 publisher = {Addison-Wesley Longman Publishing Co., Inc.},
 address = {Boston, MA, USA},
 }

@inproceedings{DBLP:conf/popl/BornatCOP05,
  author    = {Richard Bornat and
               Cristiano Calcagno and
               Peter W. O'Hearn and
               Matthew J. Parkinson},
  title     = {Permission accounting in separation logic},
  booktitle = {POPL},
  year      = {2005},
  pages     = {259-270},
  ee        = {http://doi.acm.org/10.1145/1040305.1040327},
  crossref  = {DBLP:conf/popl/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/popl/2005,
  editor    = {Jens Palsberg and
               Mart\'{\i}n Abadi},
  title     = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2005, Long Beach,
               California, USA, January 12-14, 2005},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2005},
  isbn      = {1-58113-830-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/sas/Boyland03,
  author    = {John Boyland},
  title     = {Checking Interference with Fractional Permissions},
  booktitle = {SAS},
  year      = {2003},
  pages     = {55-72},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2694/26940055.htm},
  crossref  = {DBLP:conf/sas/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sas/2003,
  editor    = {Radhia Cousot},
  title     = {Static Analysis, 10th International Symposium, SAS 2003,
               San Diego, CA, USA, June 11-13, 2003, Proceedings},
  booktitle = {SAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2694},
  year      = {2003},
  isbn      = {3-540-40325-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TECHREPORT{ParkinsonDissertation,
    author = {Matthew J. Parkinson},
    title = {Local Reasoning for {Java}},
    institution = {University of Cambridge},
    year = {2005},
    note = {Technical Report UCAM-CL-TR-64}
}

@inproceedings{DBLP:conf/vstte/Ridge10,
  author    = {Tom Ridge},
  title     = {A Rely-Guarantee Proof System for x86-{TSO}},
  booktitle = {VSTTE},
  year      = {2010},
  pages     = {55-70},
  ee        = {http://dx.doi.org/10.1007/978-3-642-15057-9_4},
  crossref  = {DBLP:conf/vstte/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/vstte/2010,
  editor    = {Gary T. Leavens and
               Peter W. O'Hearn and
               Sriram K. Rajamani},
  title     = {Verified Software: Theories, Tools, Experiments, Third International
               Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010.
               Proceedings},
  booktitle = {VSTTE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6217},
  year      = {2010},
  isbn      = {978-3-642-15056-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-15057-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tcs/Brookes07,
  author    = {Stephen Brookes},
  title     = {A semantics for concurrent separation logic},
  journal   = {Theor. Comput. Sci.},
  volume    = {375},
  number    = {1-3},
  year      = {2007},
  pages     = {227-270},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.12.034},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/entcs/GotsmanBC11,
  author    = {Alexey Gotsman and
               Josh Berdine and
               Byron Cook},
  title     = {Precision and the Conjunction Rule in Concurrent Separation
               Logic},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {276},
  year      = {2011},
  pages     = {171-190},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2011.09.021},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/aplas/DockinsHA09,
  author    = {Robert Dockins and
               Aquinas Hobor and
               Andrew W. Appel},
  title     = {A Fresh Look at Separation Algebras and Share Accounting},
  booktitle = {APLAS},
  year      = {2009},
  pages     = {161-177},
  ee        = {http://springerlink.metapress.com/content/rp5547377166x21j/},
  crossref  = {DBLP:conf/aplas/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aplas/2009,
  editor    = {Zhenjiang Hu},
  title     = {Programming Languages and Systems, 7th Asian Symposium,
               APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings},
  booktitle = {APLAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5904},
  year      = {2009},
  isbn      = {978-3-642-10671-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-10672-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TECHREPORT{Plotkin:NatSemTR,
  AUTHOR = {Gordon D. Plotkin},
  TITLE = {A Structural Approach to Operational Semantics},
  ADDRESS = {Aarhus, Denmark},
  INSTITUTION = {Computer Science Department, Aarhus University},
  YEAR = {1981},
  MONTH = SEP,
  NUMBER = {DAIMI FN--19}
}

@inproceedings{DBLP:conf/itp/CohenS10,
  author    = {Ernie Cohen and
               Bert Schirmer},
  title     = {From Total Store Order to Sequential Consistency: A Practical
               Reduction Theorem},
  booktitle = {ITP},
  year      = {2010},
  pages     = {403-418},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14052-5_28},
  crossref  = {DBLP:conf/itp/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itp/2010,
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  title     = {Interactive Theorem Proving, First International Conference,
               ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6172},
  year      = {2010},
  isbn      = {978-3-642-14051-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14052-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DPN93, 
	author = {David Dill and SeungJoon Park and Andreas Nowatzyk}, 
	title = {Formal Specification of Abstract Memory Models}, 
	booktitle = {Research on Integrated Systems}, 
	publisher = {MIT Press}, 
	editors = {G. Borriello and C. Ebeling}, 
	year = {1993}
}

@phdthesis{ChatterjeeDissertation,
    author = {Prosenjit Chatterjee},
    title = {Formal Specification and Verification of Memory Consistency Models of Shared Memory Multiprocessors},
    school = {The University of Utah},
    year = {2002}
}

@proceedings{MFPS11,
  editor    = {Joel Ouaknine},
  title     = {27th Conference on the Mathematical Foundations of Programming Semantics},
  booktitle = {MFPS},
  year      = {2011},
}

@inproceedings{V11,
	author = {Viktor Vafeiadis}, 
	title = {Concurrent separation logic and operational semantics},
	booktitle = {27th Conference on the Mathematical Foundations of Programming Semantics},
	editor = {Jo{\"e}l Ouaknine},
	year = {2011},
}

@INPROCEEDINGS{Girard95logic,
    author = {Jean-Yves Girard},
    title = {Linear Logic: Its Syntax and Semantics},
    booktitle = {Advances in Linear Logic},
    year = {1995},
    pages = {1--42},
    publisher = {Cambridge University Press}
}

@inproceedings{DBLP:conf/RelMiCS/HoareMSW09,
  author    = {C. A. R. Hoare and
               Bernhard M{\"o}ller and
               Georg Struth and
               Ian Wehrman},
  title     = {Foundations of Concurrent Kleene Algebra},
  booktitle = {RelMiCS},
  year      = {2009},
  pages     = {166-186},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04639-1_12},
  crossref  = {DBLP:conf/RelMiCS/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/RelMiCS/2009,
  editor    = {Rudolf Berghammer and
               Ali Jaoua and
               Bernhard M{\"o}ller},
  title     = {Relations and Kleene Algebra in Computer Science, 11th International
               Conference on Relational Methods in Computer Science, RelMiCS
               2009, and 6th International Conference on Applications of
               Kleene Algebra, AKA 2009, Doha, Qatar, November 1-5, 2009.
               Proceedings},
  booktitle = {RelMiCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5827},
  year      = {2009},
  isbn      = {978-3-642-04638-4},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04639-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jlp/HoareMSW11,
  author    = {C. A. R. Hoare and
               Bernhard M{\"o}ller and
               Georg Struth and
               Ian Wehrman},
  title     = {Concurrent Kleene Algebra and its Foundations},
  journal   = {J. Log. Algebr. Program.},
  volume    = {80},
  number    = {6},
  year      = {2011},
  pages     = {266-296},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2011.04.005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{lola11,
    author = {Ian Wehrman and Josh Berdine},
    title = {A Proposal for Weak-Memory Local Reasoning},
    booktitle = {Syntax and Semantics of Low-Level Languages},
    year = {2011},
    note = "Available at \url{http://www.cs.utexas.edu/~iwehrman/pub/lola.pdf}"
}

@inproceedings{DBLP:conf/icdt/GrumbachM95,
  author    = {St{\'e}phane Grumbach and
               Tova Milo},
  title     = {An Algebra for Pomsets},
  booktitle = {ICDT},
  year      = {1995},
  pages     = {191-207},
  ee        = {http://dx.doi.org/10.1007/3-540-58907-4_16},
  crossref  = {DBLP:conf/icdt/95},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icdt/95,
  editor    = {Georg Gottlob and
               Moshe Y. Vardi},
  title     = {Database Theory - ICDT'95, 5th International Conference,
               Prague, Czech Republic, January 11-13, 1995, Proceedings},
  booktitle = {ICDT},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {893},
  year      = {1995},
  isbn      = {3-540-58907-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/concur/Pratt84,
  author    = {Vaughan R. Pratt},
  title     = {The Pomset Model of Parallel Processes: Unifying the Temporal
               and the Spatial},
  booktitle = {Seminar on Concurrency},
  year      = {1984},
  pages     = {180-196},
  ee        = {http://dx.doi.org/10.1007/3-540-15670-4_9},
  crossref  = {DBLP:conf/concur/1984},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/concur/1984,
  editor    = {Stephen D. Brookes and
               A. W. Roscoe and
               Glynn Winskel},
  title     = {Seminar on Concurrency, Carnegie-Mellon University, Pittsburg,
               PA, USA, July 9-11, 1984},
  booktitle = {Seminar on Concurrency},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {197},
  year      = {1985},
  isbn      = {3-540-15670-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/Pratt82,
  author    = {Vaughan R. Pratt},
  title     = {On the Composition of Processes},
  booktitle = {POPL},
  year      = {1982},
  pages     = {213-223},
  ee        = {http://doi.acm.org/10.1145/582153.582177},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/concur/HoareHMOPS11,
  author    = {C. A. R. Hoare and
               Akbar Hussain and
               Bernhard M{\"o}ller and
               Peter W. O'Hearn and
               Rasmus Lerchedahl Petersen and
               Georg Struth},
  title     = {On Locality and the Exchange Law for Concurrent Processes},
  booktitle = {CONCUR},
  year      = {2011},
  pages     = {250-264},
  ee        = {http://dx.doi.org/10.1007/978-3-642-23217-6_17},
  crossref  = {DBLP:conf/concur/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/concur/2011,
  editor    = {Joost-Pieter Katoen and
               Barbara K{\"o}nig},
  title     = {CONCUR 2011 - Concurrency Theory - 22nd International Conference,
               CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6901},
  year      = {2011},
  isbn      = {978-3-642-23216-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-23217-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tlca/RetoreL97,
  author    = {Christian Retor{\'e} and
               Pomset Logic},
  title     = {A Non-commutative Extension of Classical Linear Logic},
  booktitle = {TLCA},
  year      = {1997},
  pages     = {300-318},
  ee        = {http://dx.doi.org/10.1007/3-540-62688-3_43},
  crossref  = {DBLP:conf/tlca/1997},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tlca/1997,
  editor    = {Philippe de Groote},
  title     = {Typed Lambda Calculi and Applications, Third International
               Conference on Typed Lambda Calculi and Applications, TLCA
               '97, Nancy, France, April 2-4, 1997, Proceedings},
  booktitle = {TLCA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1210},
  year      = {1997},
  isbn      = {3-540-62688-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Brookes20115,
title = "A Revisionist History of Concurrent Separation Logic",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "276",
number = "0",
pages = "5 - 28",
year = "2011",
note = "Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII)",
issn = "1571-0661",
doi = "10.1016/j.entcs.2011.09.013",
url = "http://www.sciencedirect.com/science/article/pii/S1571066111001046",
author = "Stephen Brookes",
keywords = "concurrency",
keywords = "shared memory",
keywords = "denotational semantics",
keywords = "resources",
keywords = "separation logic"
}

@inproceedings{DBLP:conf/popl/ReddyR12,
  author    = {Uday S. Reddy and
               John C. Reynolds},
  title     = {Syntactic control of interference for separation logic},
  booktitle = {POPL},
  year      = {2012},
  pages     = {323-336},
  ee        = {http://doi.acm.org/10.1145/2103656.2103695},
  crossref  = {DBLP:conf/popl/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/popl/2012,
  editor    = {John Field and
               Michael Hicks},
  title     = {Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2012, Philadelphia,
               Pennsylvania, USA, January 22-28, 2012},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1083-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/fossacs/YangO02,
  author    = {Hongseok Yang and
               Peter W. O'Hearn},
  title     = {A Semantic Basis for Local Reasoning},
  booktitle = {FoSSaCS},
  year      = {2002},
  pages     = {402-416},
  ee        = {http://dx.doi.org/10.1007/3-540-45931-6_28},
  crossref  = {DBLP:conf/fossacs/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fossacs/2002,
  editor    = {Mogens Nielsen and
               Uffe Engberg},
  title     = {Foundations of Software Science and Computation Structures,
               5th International Conference, FOSSACS 2002. Held as Part
               of the Joint European Conferences on Theory and Practice
               of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002,
               Proceedings},
  booktitle = {FoSSaCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2303},
  year      = {2002},
  isbn      = {3-540-43366-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/pldi/2011,
  editor    = {Mary W. Hall and
               David A. Padua},
  title     = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming
               Language Design and Implementation, PLDI 2011, San Jose,
               CA, USA, June 4-8, 2011},
  booktitle = {PLDI},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0663-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/jar/RayHMM08,
  author    = {Sandip Ray and
               Warren A. Hunt Jr. and
               John Matthews and
               J. Strother Moore},
  title     = {A Mechanical Analysis of Program Verification Strategies},
  journal   = {J. Autom. Reasoning},
  volume    = {40},
  number    = {4},
  year      = {2008},
  pages     = {245-269},
  ee        = {http://dx.doi.org/10.1007/s10817-008-9098-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/BerdineCI11,
  author    = {Josh Berdine and 
               Byron Cook and 
               Samin Ishtiaq},
  title     = {{SLAyer: Memory Safety for Systems-level Code}},
  booktitle = {CAV},
  year      = {2011},
  crossref  = {DBLP:conf/cav/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2011,
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {Computer Aided Verification - 23rd International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  year      = {2011},
  isbn      = {978-3-642-22109-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/pldi/Zeng2011,
  author    = {Qiang Zeng and
               Dinghao Wu and
               Peng Liu},
  title     = {Cruiser: Concurrent Heap Buffer Overflow Monitoring Using Lock-Free Data Structures},
  booktitle = {PLDI},
  year      = {2011},
  crossref  = {DBLP:conf/pldi/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/pldi/SarkarSAMW11,
  author    = {Susmit Sarkar and
               Peter Sewell and
               Jade Alglave and
               Luc Maranget and
               Derek Williams},
  title     = {Understanding POWER multiprocessors},
  booktitle = {PLDI},
  year      = {2011},
  pages     = {175-186},
  ee        = {http://doi.acm.org/10.1145/1993498.1993520},
  crossref  = {DBLP:conf/pldi/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/pldi/2011,
  editor    = {Mary W. Hall and
               David A. Padua},
  title     = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming
               Language Design and Implementation, PLDI 2011, San Jose,
               CA, USA, June 4-8, 2011},
  booktitle = {PLDI},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0663-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/computer/AdveG96,
  author    = {Sarita V. Adve and
               Kourosh Gharachorloo},
  title     = {Shared Memory Consistency Models: A Tutorial},
  journal   = {IEEE Computer},
  volume    = {29},
  number    = {12},
  year      = {1996},
  pages     = {66-76},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/2.546611},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Leroy-Compcert-CACM,
  author = {Xavier Leroy},
  title = {Formal verification of a realistic compiler},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
  pubkind = {journal-int-mono},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.}
}

@inproceedings{DBLP:conf/mpc/Bornat00,
  author    = {Richard Bornat},
  title     = {Proving Pointer Programs in Hoare Logic},
  booktitle = {MPC},
  year      = {2000},
  pages     = {102-126},
  ee        = {http://dx.doi.org/10.1007/10722010_8},
  crossref  = {DBLP:conf/mpc/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/mpc/2000,
  editor    = {Roland Carl Backhouse and
               Jos{\'e} Nuno Oliveira},
  title     = {Mathematics of Program Construction, 5th International Conference,
               MPC 2000, Ponte de Lima, Portugal, July 3-5, 2000, Proceedings},
  booktitle = {MPC},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1837},
  year      = {2000},
  isbn      = {3-540-67727-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/fsttcs/GalmicheL06,
  author    = {Didier Galmiche and
               Dominique Larchey-Wendling},
  title     = {Expressivity properties of Boolean {BI} through Relational Models},
  booktitle = {FSTTCS},
  year      = {2006},
  pages     = {357-368},
  ee        = {http://dx.doi.org/10.1007/11944836_33},
  crossref  = {DBLP:conf/fsttcs/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fsttcs/2006,
  editor    = {S. Arun-Kumar and
               Naveen Garg},
  title     = {FSTTCS 2006: Foundations of Software Technology and Theoretical
               Computer Science, 26th International Conference, Kolkata,
               India, December 13-15, 2006, Proceedings},
  booktitle = {FSTTCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4337},
  year      = {2006},
  isbn      = {3-540-49994-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/ipl/Peterson81,
  author    = {Gary L. Peterson},
  title     = {Myths About the Mutual Exclusion Problem},
  journal   = {Inf. Process. Lett.},
  volume    = {12},
  number    = {3},
  year      = {1981},
  pages     = {115-116},
  ee        = {http://dx.doi.org/10.1016/0020-0190(81)90106-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{DBLP:series/natosec/HoareW11,
  author    = {Tony Hoare and
               John Wickerson},
  title     = {Unifying Models of Data Flow},
  booktitle = {Software and Systems Safety - Specification and Verification},
  year      = {2011},
  pages     = {211-230},
  ee        = {http://dx.doi.org/10.3233/978-1-60750-711-6-211},
  crossref  = {DBLP:series/natosec/30},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@book{DBLP:series/natosec/30,
  editor    = {Manfred Broy and
               Christian Leuxner and
               Tony Hoare},
  title     = {Software and Systems Safety - Specification and Verification},
  booktitle = {Software and Systems Safety - Specification and Verification},
  publisher = {IOS Press},
  series    = {NATO Science for Peace and Security Series - D: Information
               and Communication Security},
  volume    = {30},
  year      = {2011},
  isbn      = {978-1-60750-710-9},
  ee        = {http://dx.doi.org/10.3233/978-1-60750-711-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ac/Winskel86,
  author    = {Glynn Winskel},
  title     = {Event Structures},
  booktitle = {Advances in Petri Nets},
  year      = {1986},
  pages     = {325-392},
  ee        = {http://dx.doi.org/10.1007/3-540-17906-2_31},
  crossref  = {DBLP:conf/ac/1986petri2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ac/1986petri2,
  editor    = {Wilfried Brauer and
               Wolfgang Reisig and
               Grzegorz Rozenberg},
  title     = {Petri Nets: Central Models and Their Properties, Advances
               in Petri Nets 1986, Part II, Proceedings of an Advanced
               Course, Bad Honnef, 8.-19. September 1986},
  booktitle = {Advances in Petri Nets},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {255},
  year      = {1987},
  isbn      = {3-540-17906-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/esop/DoddsFPV09,
  author    = {Mike Dodds and
               Xinyu Feng and
               Matthew J. Parkinson and
               Viktor Vafeiadis},
  title     = {Deny-Guarantee Reasoning},
  booktitle = {ESOP},
  year      = {2009},
  pages     = {363-377},
  ee        = {http://dx.doi.org/10.1007/978-3-642-00590-9_26},
  crossref  = {DBLP:conf/esop/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/esop/2009,
  editor    = {Giuseppe Castagna},
  title     = {Programming Languages and Systems, 18th European Symposium
               on Programming, ESOP 2009, Held as Part of the Joint European
               Conferences on Theory and Practice of Software, ETAPS 2009,
               York, UK, March 22-29, 2009. Proceedings},
  booktitle = {ESOP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5502},
  year      = {2009},
  isbn      = {978-3-642-00589-3},
  ee        = {http://dx.doi.org/10.1007/978-3-642-00590-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/jvm/MooreP01,
  author    = {J. Strother Moore and
               George Porter},
  title     = {An Executable Formal Java Virtual Machine Thread Model},
  booktitle = {Java Virtual Machine Research and Technology Symposium},
  year      = {2001},
  pages     = {91-104},
  ee        = {http://www.usenix.org/publications/library/proceedings/jvm01/moore.html},
  crossref  = {DBLP:conf/jvm/2001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/jvm/2001,
  title     = {Proceedings of the 1st Java Virtual Machine Research
               and Technology Symposium, April 23-24, 2001, Monterey, CA,
               USA},
  booktitle = {Java Virtual Machine Research and Technology Symposium},
  publisher = {USENIX},
  year      = {2001},
  isbn      = {1-880446-11-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ecoop/Owens10,
  author    = {Scott Owens},
  title     = {Reasoning about the Implementation of Concurrency Abstractions
               on x86-TSO},
  booktitle = {ECOOP},
  year      = {2010},
  pages     = {478-503},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14107-2_23},
  crossref  = {DBLP:conf/ecoop/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ecoop/2010,
  editor    = {Theo D'Hondt},
  title     = {ECOOP 2010 - Object-Oriented Programming, 24th European
               Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings},
  booktitle = {ECOOP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6183},
  year      = {2010},
  isbn      = {978-3-642-14106-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-14107-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}