@Book{Paulson96,
  author = 	 {L.~C.~Paulson},
  title = 	 {{ML} for the {W}orking {P}rogrammer},
  publisher = 	 {Cambridge University Press},
  year = 	 {1996}
}


@Manual{LINUX,
  author =       {S.~Rostedt},
  title =        {{RT}-{M}utex {I}mplementation {D}esign},
  note =         {Linux Kernel Distribution at, 
                  www.kernel.org/doc/Documentation/rt-mutex-design.txt}
}

@Misc{PINTOS,
  author = {B.~Pfaff},
  title = {{PINTOS}}, 
  note = {\url{http://www.stanford.edu/class/cs140/projects/}},
}


@inproceedings{Haftmann08,
  author    = {F.~Haftmann and M.~Wenzel},
  title     = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar},
  booktitle = {Proc.~of the International Conference on Types, Proofs and Programs (TYPES)},
  year      = {2008},
  pages     = {153-168},
  series    = {LNCS},
  volume    = {5497}
}


@TechReport{Yodaiken02,
  author =       {V.~Yodaiken},
  title =        {{A}gainst {P}riority {I}nheritance},
  institution =  {Finite State Machine Labs (FSMLabs)},
  year =         {2004}
}


@Book{Vahalia96,
  author =       {U.~Vahalia},
  title =        {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers},
  publisher =    {Prentice-Hall},
  year =         {1996}
}

@Article{Reeves98,
  title =	"{R}e: {W}hat {R}eally {H}appened on {M}ars?",
  author =	"G.~E.~Reeves",
  journal =	"Risks Forum",
  year = 	"1998",
  number =	"54",
  volume =	"19"
}

@Article{Sha90,
  title =	"{P}riority {I}nheritance {P}rotocols: {A}n {A}pproach to
		 {R}eal-{T}ime {S}ynchronization",
  author =	"L.~Sha and R.~Rajkumar and J.~P.~Lehoczky",
  journal =	"IEEE Transactions on Computers",
  year = 	"1990",
  number =	"9",
  volume =	"39",
  pages =	"1175--1185"
}


@Article{Lampson80,
  author =	"B.~W.~Lampson and D.~D.~Redell",
  title =	"{{E}xperiences with {P}rocesses and {M}onitors in {M}esa}",
  journal =	"Communications of the ACM",
  volume =	"23",
  number =	"2",
  pages =	"105--117",
  year = 	"1980"
}

@inproceedings{Wang09,
  author    = {J.~Wang and H.~Yang and X.~Zhang},
  title     = {{L}iveness {R}easoning with {I}sabelle/{HOL}},
  booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in 
               Higher Order Logics (TPHOLs)},
  year      = {2009},
  pages     = {485--499},
  volume    = {5674},
  series    = {LNCS}
}

@PhdThesis{Faria08,
  author =       {J.~M.~S.~Faria},
  title =        {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems 
                 with {TLA+/TLC}},
  school =       {University of Porto},
  year =         {2008}
}


@Article{Paulson98,
  author =       {L.~C.~Paulson},
  title =        {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols},
  journal =      {Journal of Computer Security},
  year =         {1998},
  volume =       {6},
  number =       {1--2},
  pages =        {85--128}
}

@MISC{locke-july02,
author = {D. Locke},
title = {Priority Inheritance: The Real Story},
month = July,
year = {2002},
howpublished={\url{http://www.math.unipd.it/~tullio/SCD/2007/Materiale/Locke.pdf}},
}


@InProceedings{Steinberg10,
  author =       {U.~Steinberg and A.~B\"otcher and B.~Kauer},
  title =        {{T}imeslice {D}onation in {C}omponent-{B}ased {S}ystems},
  booktitle = {Proc.~of the 6th International Workshop on Operating Systems
               Platforms for Embedded Real-Time Applications (OSPERT)},
  pages =     {16--23},
  year =      {2010}
}

@inproceedings{dutertre99b,
  title =	"{T}he {P}riority {C}eiling {P}rotocol: {F}ormalization and
		 {A}nalysis {U}sing {PVS}",
  author =	"B.~Dutertre",
  booktitle = {Proc.~of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS)},
  year = {2000},
  pages = {151--160},
  publisher = {IEEE Computer Society}
}

@InProceedings{Jahier09,
  title =	"{S}ynchronous {M}odeling and {V}alidation of {P}riority
		 {I}nheritance {S}chedulers",
  author =	"E.~Jahier and B.~Halbwachs and P.~Raymond",
  booktitle =	"Proc.~of the 12th International Conference on Fundamental 
                 Approaches to Software Engineering (FASE)",
  year = 	"2009",
  volume =	"5503",
  series =      "LNCS",
  pages =	"140--154"
}

@InProceedings{Wellings07,
  title =	"{I}ntegrating {P}riority {I}nheritance {A}lgorithms in the {R}eal-{T}ime 
                 {S}pecification for {J}ava",
  author =	"A.~Wellings and A.~Burns and O.~M.~Santos and B.~M.~Brosgol",
  publisher =	"IEEE Computer Society",
  year = 	"2007",
  booktitle =	"Proc.~of the 10th IEEE International Symposium on Object 
                and Component-Oriented Real-Time Distributed Computing (ISORC)",
  pages =	"115--123"
}

@Article{Wang:2002:SGP,
  author =	"Y. Wang and E. Anceaume and F. Brasileiro and F.
		 Greve and M. Hurfin",
  title =	"Solving the group priority inversion problem in a
		 timed asynchronous system",
  journal =	"IEEE Transactions on Computers",
  volume =	"51",
  number =	"8",
  pages =	"900--915",
  month =	aug,
  year = 	"2002",
  CODEN =	"ITCOB4",
  doi =  	"http://dx.doi.org/10.1109/TC.2002.1024738",
  ISSN = 	"0018-9340 (print), 1557-9956 (electronic)",
  issn-l =	"0018-9340",
  bibdate =	"Tue Jul 5 09:41:56 MDT 2011",
  bibsource =	"http://www.computer.org/tc/;
		 http://www.math.utah.edu/pub/tex/bib/ieeetranscomput2000.bib",
  URL =  	"http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1024738",
  acknowledgement = "Nelson H. F. Beebe, University of Utah, Department
		 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
		 \path|beebe@acm.org|, \path|beebe@computer.org|
		 (Internet), URL:
		 \path|http://www.math.utah.edu/~beebe/|",
  fjournal =	"IEEE Transactions on Computers",
  doi-url =	"http://dx.doi.org/10.1109/TC.2002.1024738",
}

@Article{journals/rts/BabaogluMS93,
  title =	"A Formalization of Priority Inversion",
  author =	"{\"O} Babaoglu and K. Marzullo and F. B. Schneider",
  journal =	"Real-Time Systems",
  year = 	"1993",
  number =	"4",
  volume =	"5",
  bibdate =	"2011-06-03",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/journals/rts/rts5.html#BabaogluMS93",
  pages =	"285--303",
  URL =  	"http://dx.doi.org/10.1007/BF01088832",
}