@STRING{cacm="Communications of the ACM"}
@STRING{csur="{ACM} Computing Surveys"}
@STRING{fac="Formal Aspects of Computing"}
@STRING{ipl="Information Processing Letters"}
@STRING{lncs="LNCS"}
@STRING{tcs="Theoretical Computer Science"}

@article{AptFrancezDeRoever:1980,
  author =       {K. R. Apt and Francez, N. and de Roever, W. P.},
  title =        {A Proof System for Communicating Sequential
                  Processes},
  journal =      toplas,
  year =         1980,
  volume =       2,
  number =       3,
  pages =        {359--385},
  doi =          {10.1145/357103.357110}
}

@TechReport{LynchTuttle:1989,
  author =       "Lynch, N. A and Tuttle, M. R.",
  title =        "An introduction to input/output automata",
  institution =  "CWI",
  year =         1989,
  month =     sep,
  annote =    "CWI Quarterly 2 (3): 219--246",
  url = "http://www.markrtuttle.com/data/papers/lt89-cwi.pdf"
}

@book{Lynch:1996,
 author = {N. A. Lynch},
 title = {Distributed Algorithms},
 year = 1996,
 publisher = {Morgan Kaufmann Publishers Inc.},
}

@InProceedings{PrenEsp00,
  author =    {Prensa Nieto, L. and J. Esparza},
  title =     {Verifying Single and Multi-mutator Garbage Collectors
                with {Owicki/Gries} in {Isabelle/HOL}},
  booktitle = {Mathematical Foundations of Computer Science (MFCS 2000)},
  editor =    {M. Nielsen and B. Rovan},
  publisher = {Springer},
  series =    lncs,
  volume =    1893,
  pages =     {619--628},
  year =      2000
}

@PhdThesis{Prensa-PhD,
  author={Prensa Nieto, L.},
  title={Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL},
  school={Technische Universit{\"a}t M{\"u}nchen},
  year=2002
}

@inproceedings{Prensa-ESOP03,
  author={Prensa Nieto, L.},
  title={The {Rely-Guarantee} Method in {Isabelle/HOL}},
  booktitle={ESOP'2003},
  editor={P. Degano},
  publisher="Springer",
  series=lncs,volume=2618,
  pages={348--362},
  year=2003
}

@book{Winskel:1993,
 author = {Winskel, G.},
 title = {The Formal Semantics of Programming Languages},
 year = 1993,
 publisher = {MIT Press},
 address = "Cambridge, MA"
}

@article{DBLP:journals/cacm/DijkstraLMSS78,
  author    = {E. W. Dijkstra and
               L. 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,
  year      = 1978,
  pages     = {966-975},
  ee        = {http://doi.acm.org/10.1145/359642.359655},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lpar/Schirmer04,
  author    = {N. Schirmer},
  title     = {A Verification Environment for Sequential Imperative Programs
               in Isabelle/HOL},
  booktitle = {LPAR},
  year      = 2004,
  pages     = {398-414},
  ee        = {https://doi.org/10.1007/978-3-540-32275-7_26},
  crossref  = {DBLP:conf/lpar/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {3-540-25236-3},
@proceedings{DBLP:conf/lpar/2004,
  editor    = {F. Baader and
               A. Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               11th International Conference, LPAR 2004, Montevideo, Uruguay,
               March 14-18, 2005, Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = lncs,
  volume    = {3452},
  year      = {2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/cacm/SewellSONM10,
  author    = {P. Sewell and
               S. Sarkar and
               S. Owens and
               F. Zappa Nardelli and
               M. O. Myreen},
  title     = {{x86-TSO}: a rigorous and usable programmer's model for x86
               multiprocessors},
  journal   = cacm,
  volume    = {53},
  number    = {7},
  year      = {2010},
  pages     = {89-97},
  ee        = {http://doi.acm.org/10.1145/1785414.1785443},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/mfcs/BoerRH99,
  author    = {de Boer, F. S. and
               de Roever, W. P. and
               U. Hannemann},
  title     = {The Semantic Foundations of a Compositional Proof Method
               for Synchronously Communicating Processes},
  booktitle = {MFCS},
  year      = {1999},
  pages     = {343-353},
  ee        = {https://doi.org/10.1007/3-540-48340-3_31},
  crossref  = {DBLP:conf/mfcs/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {3-540-66408-4},
@proceedings{DBLP:conf/mfcs/1999,
  editor    = {M. Kutylowski and
               L. Pacholski and
               T. Wierzbicki},
  title     = {Mathematical Foundations of Computer Science 1999, 24th
               International Symposium, MFCS'99, Szklarska Poreba, Poland,
               September 6-10, 1999, Proceedings},
  booktitle = {MFCS},
  publisher = {Springer},
  series    = lncs,
  volume    = {1672},
  year      = {1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {0-521-80608-9},
@book{deRoeverEtAl:2001,
  author    = {de Roever, W. P. and
               de Boer, F. S. and
               U. Hannemann and
               J. Hooman and
               Y. Lakhnech and
               M. Poel and
               J. Zwiers},
  title     = {Concurrency Verification: Introduction to Compositional
               and Noncompositional Methods},
  publisher = {Cambridge University Press},
  series    = {Cambridge Tracts in Theoretical Computer Science},
  volume    = 54,
  year      = 2001,
}

@InProceedings{Pizlo+2010PLDI,
author =	 {F. Pizlo and L. Ziarek and P. Maj and A.
                L. Hosking and E. Blanton and J. Vitek},
title =	 {Schism: Fragmentation-Tolerant Real-Time Garbage Collection},
booktitle =	 {Proceedings of the ACM SIGPLAN Conference on Programming
                Language Design and Implementation},
year =	 2010,
pages =	 "146--159",
month =	 jun,
address =	 {Toronto, Canada},
doi =		 {10.1145/1806596.1806615}
}

@PhdThesis{Pizlo201xPhd,
author =	 {F. Pizlo},
title =	 {Fragmentation Tolerant Real Time Garbage Collection},
school =	 {Purdue University},
year =	 {201x}
}

@article{DBLP:journals/toplas/LamportS84,
  author    = {L. Lamport and F. B. Schneider},
  title     = {The ``{Hoare Logic}'' of {CSP}, and All That},
  journal   = toplas,
  volume    = {6},
  number    = {2},
  year      = {1984},
  pages     = {281-296},
  ee        = {http://doi.acm.org/10.1145/2993.357247},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/acta/Lamport80,
  author    = {L. Lamport},
  title     = {The ``{Hoare Logic}'' of Concurrent Programs},
  journal   = {Acta Informatica},
  volume    = {14},
  year      = {1980},
  pages     = {21-37},
  ee        = {https://doi.org/10.1007/BF00289062},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/Berghofer12,
  author    = {S. Berghofer},
  title     = {A Solution to the {PoplMark} Challenge Using {de Bruijn} Indices
               in {Isabelle/HOL}},
  journal   = {J. Autom. Reasoning},
  volume    = {49},
  number    = {3},
  year      = {2012},
  pages     = {303-326},
  ee        = {https://doi.org/10.1007/s10817-011-9231-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn =	 {3-540-44044-5}
@InCollection{PittsAM:opespe,
  author =	 {A. M. Pitts},
  title =	 {Operational Semantics and Program Equivalence},
  booktitle =	 {Applied Semantics, Advanced Lectures},
  pages =	 {378--412},
  publisher =	 {Springer},
  year =	 2002,
  editor =	 {G. Barthe and P. Dybjer and J. Saraiva},
  volume =	 2395,
  series =	 lncs,
  note =	 {International Summer School, {APPSEM} 2000, Caminha,
                  Portugal, September 9--15, 2000},
}

@InCollection{MannaPnueli:1991,
  author =       "Z. Manna and A. Pnueli",
  title =        "Tools and rules for the practicing verifier",
  booktitle =    "CMU Computer Science: A 25th Anniversary Commemorative",
  pages =     "121--156",
  publisher = "ACM Press and Addison-Wesley",
  year =      1991,
  editor =    "R. F. Rashid",
  note = "Also Technical Report STAN-CS-90-1321"
}

%  isbn      = {978-0-387-94459-3},
@book{MannaPnueli:1995,
  author    = {Z. Manna and A. Pnueli},
  title     = {Temporal verification of reactive systems - {Safety}},
  publisher = {Springer},
  year      = 1995,
  pages     = {I-XV, 1-512},
}

@inproceedings{MannaPnueli:2010,
  author    = {Z. Manna and A. Pnueli},
  title     = {Temporal Verification of Reactive Systems: Response},
  booktitle = {Time for Verification, Essays in Memory of Amir Pnueli},
  series    = lncs,
  volume    = 6200,
  publisher = {Springer},
  pages     = {279--361},
  year      = 2010,
  doi       = {10.1007/978-3-642-13754-9\_13},
}

@article{DBLP:journals/acta/LevinG81,
  author    = {G. Levin and
               D. Gries},
  title     = {A Proof Technique for Communicating Sequential Processes},
  journal   = {Acta Inf.},
  volume    = {15},
  year      = {1981},
  pages     = {281-302},
  ee        = {https://doi.org/10.1007/BF00289266},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CousotCousot:1980,
  author    = {P. Cousot and R. Cousot},
  title     = "Semantic Analysis of {Communicating Sequential Processes}
               (Shortened Version)",
  booktitle = {ICALP},
  series    = lncs,
  volume    = {85},
  publisher = {Springer},
  year      = 1980,
  pages     = {119-133},
  ee        = {https://doi.org/10.1007/3-540-10003-2_65},
}

%  isbn      = {0-3211-4306-X},
@book{Lamport:2002,
  author    = {L. Lamport},
  title     = {Specifying Systems, The TLA+ Language and Tools for Hardware
               and Software Engineers},
  publisher = {Addison-Wesley},
  year      = 2002
}

@article{TLA-AFP,
  author  = {G. Grov and S. Merz},
  title   = {A Definitional Encoding of TLA* in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2011,
  note    = {\url{http://isa-afp.org/entries/TLA},
            Formal proof development},
  ISSN    = {2150-914x},
}

@inproceedings{DBLP:conf/itp/CohenS10,
  author    = {E. Cohen and
               B. Schirmer},
  title     = {From Total Store Order to Sequential Consistency: A Practical
               Reduction Theorem},
  booktitle = {ITP},
  year      = {2010},
  pages     = {403-418},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5_28},
  crossref  = {DBLP:conf/itp/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-3-642-14051-8},
@proceedings{DBLP:conf/itp/2010,
  editor    = {M. Kaufmann and
               L. C. Paulson},
  title     = {Interactive Theorem Proving, First International Conference,
               ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = lncs,
  volume    = {6172},
  year      = {2010},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/fase/NipkowN99,
  author    = {T. Nipkow and
               Prensa Nieto, L.},
  title     = "{Owicki/Gries} in {Isabelle/HOL}",
  booktitle = {FASE},
  year      = {1999},
  pages     = {188-203},
  ee        = {https://doi.org/10.1007/978-3-540-49020-3_13},
  crossref  = {DBLP:conf/fase/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {3-540-65718-5},
@proceedings{DBLP:conf/fase/1999,
  editor    = {J.-P. Finance},
  title     = {Fundamental Approaches to Software Engineering, Second Internationsl
               Conference, FASE'99, Held as Part of the European Joint
               Conferences on the Theory and Practice of Software, ETAPS'99,
               Amsterdam, The Netherlands, March 22-28, 1999, Proceedings},
  booktitle = {FASE},
  publisher = {Springer},
  series    = lncs,
  volume    = {1577},
  year      = {1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{CousotCousot89-IC,
   author =  {Cousot, P. and Cousot, R.},
   title =   {A language independent proof of the soundness
              and completeness of generalized {H}oare logic},
   journal = {Information and Computation},
   volume =  80,
   number =  2,
   pages =   {165--191},
   month =   feb,
   year =    1989,
}

@article{DBLP:journals/jlp/Plotkin04,
  author    = {G. D. Plotkin},
  title     = {The origins of structural operational semantics},
  journal   = {Journal of Logic and Algebraic Programming},
  volume    = {60-61},
  year      = {2004},
  pages     = {3-15},
  ee        = {https://doi.org/10.1016/j.jlap.2004.03.009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{ConcreteSemantics:2014,
  author =       "T. Nipkow and G. Klein",
  title =        "Concrete Semantics: A Proof Assistant Approach",
  publisher =    "Springer",
  year =         2014,
  url = "http://www.in.tum.de/~nipkow/Concrete-Semantics/"
}

@Book{Hoare:1985,
  author       = {C.A.R. Hoare},
  title        = "{Communicating Sequential Processes}",
  publisher    = {Prentice-Hall},
  year         = 1985,
  series       = {International Series In Computer Science},
  url = "http://www.usingcsp.com/"
}

@Book{Milner:1980,
  author =       "R. Milner",
  title =        "A Calculus of Communicating Systems",
  publisher =    "Springer",
  year =         1980
}

@book{Milner:1989,
 author = {R. Milner},
 title = "Communication and Concurrency",
 year = {1989},
 publisher = {Prentice-Hall},
 address = "Englewood Cliffs, NJ",
}

@article{FelleisenHieb:1992,
  author    = {M. Felleisen and
               R. Hieb},
  title     = {The Revised Report on the Syntactic Theories of Sequential
               Control and State},
  journal   = tcs,
  volume    = 103,
  number    = 2,
  year      = 1992,
  pages     = {235-271},
  doi       = {10.1016/0304-3975(92)90014-7},
}

@inproceedings{Jackson:1998,
  author    = {P. B. Jackson},
  title     = {Verifying a Garbage Collection Algorithm},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = lncs,
  volume    = {1479},
  year      = 1998,
  pages     = {225-244},
  doi       = {10.1007/BFb0055139},
}

@article{CoupetGrimal:2003,
  author    = {Coupet-Grimal, S.},
  title     = {An Axiomatization of {Linear Temporal Logic} in the {Calculus
               of Inductive Constructions}},
  journal   = {Journal of Logic and Computation},
  volume    = 13,
  number    = 6,
  year      = 2003,
  pages     = {801-813},
  doi       = {10.1093/logcom/13.6.801},
}

@article{DBLP:journals/entcs/SchirmerW09,
  author    = {N. Schirmer and
               M. Wenzel},
  title     = {State Spaces - The Locale Way},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {254},
  year      = {2009},
  pages     = {161-179},
  ee        = {https://doi.org/10.1016/j.entcs.2009.09.065},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Ridge:2009,
  author    = {T. Ridge},
  title     = {Verifying distributed systems: the operational approach},
  booktitle = {POPL'2009},
  pages     = {429--440},
  publisher = {{ACM}},
  year      = 2009,
  doi       = {10.1145/1480881.1480934},
}

@book{ChandyMisra:1989,
  author    = {Chandy, K. M. and Misra, J.},
  title     = {Parallel program design - a foundation},
  publisher = {Addison-Wesley},
  year      = 1989,
  isbn      = {978-0-201-05866-6},
}

% 2019-06 FIXME not yet published?
@Article{vanGlabbeekHofner:2019,
  author =       {van Glabbeek, R. J. and H\"{o}fner, P.},
  title =        {Progress, Justness and Fairness},
  journal =      csur,
  year =         2019,
  url = {http://arxiv.org/abs/1810.07414v1}
}

@article{AptDelporteGallet:1986,
  author    = {Krzysztof R. Apt and
               Carole Delporte{-}Gallet},
  title     = {Syntax Directed Analysis of Liveness Properties},
  journal   = {Information and Control},
  volume    = 68,
  number    = {1-3},
  pages     = {223--253},
  year      = 1986,
  doi       = {10.1016/S0019-9958(86)80037-7},
}

@inproceedings{MisraChandySmith:1982,
  author    = {J. Misra and
               K. M. Chandy and
               T. Smith},
  title     = {Proving Safety and Liveness of Communicating Processes with Examples},
  booktitle = {PODC'1982},
  publisher = {{ACM}},
  pages     = {201--208},
  year      = 1982,
  doi       = {10.1145/800220.806698},
}

@article{AlpernSchneider:1985,
  author    = {B. Alpern and
               F. B. Schneider},
  title     = {Defining Liveness},
  journal   = ipl,
  volume    = 21,
  number    = 4,
  pages     = {181--185},
  year      = 1985,
  doi       = {10.1016/0020-0190(85)90056-0},
}

@TechReport{Schneider:1987,
  author =       {F. B. Schneider},
  title =        {Decomposing Properties into Safety and Liveness using Predicate Logic},
  institution =  {Department of Computer Science, Cornell University},
  year =         1987,
  number =    {87-874},
  month =     oct
}

% FIXME guesswork on some of the biblio data
@article{Kindler:1994,
  author =       {E. Kindler},
  title =        {Safety and liveness properties: A survey},
  journal =      {Bulletin of the European Association for Theoretical Computer Science},
  year =         1994,
  volume =    53,
  number =    30,
  pages =     {268--272},
  month =     6,
  url = "http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.8206&rep=rep1&type=pdf",
}

@article{Sistla:1994,
  author    = {Sistla, A. P.},
  title     = {Safety, Liveness and Fairness in Temporal Logic},
  journal   = fac,
  volume    = 6,
  number    = 5,
  pages     = {495--512},
  year      = 1994,
  doi       = {10.1007/BF01211865},
}

@article{OwickiLamport:1982,
  author    = {S. S. Owicki and
               L. Lamport},
  title     = {Proving Liveness Properties of Concurrent Programs},
  journal   = toplas,
  volume    = 4,
  number    = 3,
  pages     = {455--495},
  year      = 1982,
  doi       = {10.1145/357172.357178},
}

@inproceedings{ChangMannaPnueli:1992,
  author    = {E. Y. Chang and
               Z. Manna and
               A. Pnueli},
  title     = {Characterization of Temporal Property Classes},
  booktitle = {ICALP'1992},
  pages     = {474--486},
  year      = 1992,
  series    = lncs,
  volume    = 623,
  publisher = {Springer},
  doi       = {10.1007/3-540-55719-9\_97},
}

@inproceedings{MannaPnueli:1988,
  author    = {Z. Manna and
               A. Pnueli},
  title     = {The anchored version of the temporal framework},
  booktitle = {Linear Time, Branching Time and Partial Order in Logics and Models
               for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands,
               May 30 - June 3, 1988, Proceedings},
  editor    = {de Bakker, J. W. and
               de Roever, W. P. and
               Rozenberg, G.},
  pages     = {201--284},
  year      = 1988,
  doi       = {10.1007/BFb0013024},
  volume    = 354,
  publisher = {Springer},
  series    = lncs,
}

@inproceedings{PnueliArons:2003,
  author="Pnueli, A. and Arons, T.",
  title="{TLPVS}: A {PVS}-Based {LTL} Verification System",
  bookTitle="Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday",
  year=2003,
  publisher="Springer",
  series=lncs,
  volume=2772,
  address="Berlin, Heidelberg",
  pages="598--625",
  abstract="In this paper we present our pvs implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive ltl system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems --- systems in which the number of processes is unbounded --- and our verification rules are appropriate to such systems.",
  isbn="978-3-540-39910-0",
  doi="10.1007/978-3-540-39910-0_26",
}

@article{AbadiPlotkin:1993,
  author    = {Mart{\'{\i}}n Abadi and
               Gordon D. Plotkin},
  title     = {A Logical View of Composition},
  journal   = tcs,
  volume    = 114,
  number    = 1,
  pages     = {3--30},
  year      = 1993,
  doi       = {10.1016/0304-3975(93)90151-I},
  note = {Journal version of FIXME Abadi, Plotkin (POPL, 1991)}
}
