paper.bib

@inproceedings{LahiriQW11,
  author    = {Shuvendu K. Lahiri and
               Shaz Qadeer and
               David Walker},
  title     = {Linear maps},
  booktitle = {PLPV},
  year      = {2011},
  pages     = {3-14}
}

@INPROCEEDINGS{Wadler90lineartypes,
    author = {Philip Wadler},
    title = {Linear Types Can Change the World!},
    booktitle = {Programming Concepts and Methods},
    year = {1990},
    publisher = {North}
}

@inproceedings{Reynolds02,
  author    = {John C. Reynolds},
  title     = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {LICS},
  year      = {2002},
  pages     = {55-74}
}

@inproceedings{VCC,
  author    = {Ernie Cohen and
               Markus Dahlweid and
               Mark A. Hillebrand and
               Dirk Leinenbach and
               Micha{\l} Moskal and
               Thomas Santen and
               Wolfram Schulte and
               Stephan Tobies},
  title     = {{VCC}: A Practical System for Verifying Concurrent {C}},
  booktitle = {TPHOLs},
  year      = {2009}
}

@inproceedings{YangH10,
  author    = {Jean Yang and
               Chris Hawblitzel},
  title     = {Safe to the last instruction: automated verification of
               a type-safe operating system},
  booktitle = {PLDI},
  year      = {2010},
  pages     = {99-110}
}

@article{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}
}

@inproceedings{MouraB08,
  author    = {Leonardo Mendon\c{c}a de Moura and
               Nikolaj Bj{\o}rner},
  title     = "{Z3: An efficient SMT solver}",
  booktitle = {TACAS},
  year      = {2008},
  pages     = {337-340}
}

@inproceedings{BarnettCDJL05,
  author    = {Michael Barnett and
               Bor-Yuh Evan Chang and
               Robert DeLine and
               Bart Jacobs and
               K. Rustan M. Leino},
  title     = {Boogie: A Modular Reusable Verifier for Object-Oriented
               Programs},
  booktitle = {FMCO},
  year      = {2005},
  pages     = {364-387}
}

@inproceedings{BL05,
  author = "Mike Barnett and K. Rustan M. Leino",
  title = "Weakest-Precondition of Unstructured Programs",
  booktitle = {PASTE},
  year = 2005
}

@book{DijkstraBook,
  author = "Edsger W. Dijkstra",
  title = "A Discipline of Programming",
  publisher = "Prentice-Hall",
  year = "1976"
}

@article{Jones83,
  author    = {Cliff B. Jones},
  title     = {Tentative Steps Toward a Development Method for Interfering
               Programs},
  journal   = {ACM TOPLAS},
  volume    = {5},
  number    = {4},
  year      = {1983},
  pages     = {596-619}
}

@article{Hoare74,
 author = {Hoare, C. A. R.},
 title = {Monitors: an operating system structuring concept},
 journal = {Commun. ACM},
 issue_date = {Oct. 1974},
 volume = {17},
 number = {10},
 month = oct,
 year = {1974},
 issn = {0001-0782},
 pages = {549--557},
 numpages = {9},
 publisher = {ACM},
 address = {New York, NY, USA}
} 

@article{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}
}

@inproceedings{ElmasQT09,
  author    = {Tayfun Elmas and
               Shaz Qadeer and
               Serdar Tasiran},
  title     = {A calculus of atomic actions},
  booktitle = {POPL},
  year      = {2009},
  pages     = {2-15}
}

@inproceedings{LM09,
 author = {Leino, K. Rustan and M\"{u}ller, Peter},
 title = {A Basis for Verifying Multi-threaded Programs},
 booktitle = {ESOP},
 year = {2009},
 pages = {378--393}
}

@inproceedings{filliatre13esop,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
  title = {Why3 --- Where Programs Meet Provers},
  booktitle = {ESOP},
  year = 2013,
  volume = {7792},
  series = {LNCS},
  publisher = {Springer},
  pages = {125--128}
}

@article{Blizard89,
author = "Wayne D. Blizard",
title = "Real-valued multisets and fuzzy sets ",
journal = "Fuzzy Sets and Systems",
volume = "33",
number = "1",
pages = "77 - 97",
year = "1989",
note = "",
issn = "0165-0114"
}

@inproceedings{boyland:03fractions,
  author =      {John Boyland},
  title =       {Checking Interference with Fractional Permissions},
  booktitle =   "Static Analysis: 10th International Symposium",
  year =        2003,
}

@inproceedings{Slayer,
  author    = {Josh Berdine and Byron Cook and Samin Ishtiaq},
  title     = {{SLAyer}: Memory Safety for Systems-level Code},
  booktitle = {CAV},
  year      = {2011}
}

@inproceedings{Cave,
  author    = {Viktor Vafeiadis},
  title     = {Automatically proving linearizability},
  booktitle = {CAV},
  year      = {2010}
}

@inproceedings{Smallfoot,
  author    = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
  title     = {Smallfoot: Modular Automatic Assertion Checking with Separation Logic},
  booktitle = {FMCO},
  year      = {2005}
}

@inproceedings{SAGL,
  author    = {Xinyu Feng and Rodrigo Ferreira and Zhong Shao},
  title     = {On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning},
  booktitle = {ESOP},
  year      = {2007}
}

@inproceedings{RGSep,
  author    = {Viktor Vafeiadis and Matthew Parkinson},
  title     = {A Marriage of Rely/Guarantee and Separation Logic},
  booktitle = {CONCUR},
  year      = {2007}
}

@inproceedings{SepLog700,
  author    = {Matthew Parkinson},
  title     = {The Next 700 Separation Logics},
  booktitle = {VSTTE},
  year      = {2010}
}

@article{SewellTSO,
author = {Peter Sewell and Susmit Sarkar and Scott Owens and Francesco Zappa Nardelli and Magnus O. Myreen},
title = "x86-{TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors",
journal = "Communications of the ACM",
volume = "53",
number = "7",
pages = "89 - 97",
year = "2010",
}

@article{FlanaganFLQ08,
  author    = {Cormac Flanagan and
               Stephen N. Freund and
               Marina Lifshin and
               Shaz Qadeer},
  title     = "Types for atomicity: Static checking and inference for Java",
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {30},
  number    = {4},
  year      = {2008}
}

@article{WrightF94,
  author    = {Andrew K. Wright and
               Matthias Felleisen},
  title     = {A Syntactic Approach to Type Soundness},
  journal   = {Inf. Comput.},
  volume    = {115},
  number    = {1},
  year      = {1994},
  pages     = {38-94}
}

@article{Jagannathan14,
  author = {Suresh Jagannathan and Vincent Laporte and Gustavo Petri and David Pichardie and Jan Vitek},
  title = {Atomicity Refinement for Verified Compilation},
  journal = {To appear in TOPLAS (presented at PLDI 2014)},
  year = {draft as of July 6, 2014}
}

@inproceedings{HenzingerHK95,
  author    = {Monika Rauch Henzinger and
               Thomas A. Henzinger and
               Peter W. Kopke},
  title     = {Computing Simulations on Finite and Infinite Graphs},
  booktitle = {FOCS},
  year      = {1995},
}

@article{Lipton75,
  author    = {Richard J. Lipton},
  title     = {Reduction: A Method of Proving Properties of Parallel Programs},
  journal   = {Commun. ACM},
  volume    = {18},
  number    = {12},
  year      = {1975},
  pages     = {717-721}
}

@article{dijk78,
  author =	 "Edsgar W. Dijkstra and Leslie Lamport and A. J. Martin and
                  C. S. Scholten and E. F. M. Steffens",
  title =	 "On-The-Fly Garbage Collection: An exercise in Cooperation",
  journal =	 CACM,
  volume =	 21,
  number =	 11,
  month =	 Nov,
  year =	 1978,
}

@inproceedings{doli93,
title = "A Concurrent Generational Garbage Collector for a Multi-Threaded Implementation of {ML}",
author = "Damien Doligez and Xavier Leroy",
booktitle = {POPL},
year = 1993
}

@inproceedings{doli94,
title = "Portable, Unobtrusive Garbage Collection for Multiprocessor Systems",
author = "Damien Doligez and Georges Gonthier",
booktitle = {POPL},
year = 1994
}

@inproceedings{doma00,
  title =	 {A Generational On-the-fly Garbage Collector for {J}ava},
  author =	 {Tamar Domani and Elliot K. Kolodner and Erez Petrank},
  booktitle = {PLDI},
  year = 2000
}

@inproceedings{azat03,
author = {Hezi Azatchi and Yossi Levanoni and Harel Paz and Erez Petrank},
title = {An On-The-Fly Mark and Sweep Garbage Collector Based on Sliding Views},
booktitle = {OOPSLA},
year = 2003
}

@inproceedings{gont96,
author = {Georges Gonthier},
title = {Verifying the Safety of a Practical Concurrent Garbage Collector},
booktitle = {CAV},
year = 1996
}

@inproceedings{mccr07,
  title =	 {A General Framework for Certifying Garbage Collectors and
                  Their Mutators},
  author =	 {Andrew McCreight and Zhong Shao and Chunxiao Lin and Long
                  Li},
  booktitle =	 {PLDI},
  year = 2007
}

@inproceedings{hawb09,
title = {Automated Verification of Practical Garbage Collectors},
author = {Chris Hawblitzel and Erez Petrank},
booktitle = {POPL},
year = 2009
}

@article{FlanaganFQS05,
  author    = {Cormac Flanagan and
               Stephen N. Freund and
               Shaz Qadeer and
               Sanjit A. Seshia},
  title     = {Modular verification of multithreaded programs},
  journal   = {Theor. Comput. Sci.},
  volume    = {338},
  number    = {1-3},
  year      = {2005},
  pages     = {153-183}
}