%%====================================================================== %% WARNING: Do NOT edit this file. It was produced automatically %% with the UNIX pipeline %% %% biblex xxx.bib | \ %% gawk -f keywords.awk | \ %% egrep 'entrytype$' | \ %% gawk -f fmtwords.awk >xxx.xwx %% %% by beebe@gamma.math.utah.edu on Tue Feb 20 16:40:34 MST 2024 %%====================================================================== \ifx \NAMECITE \undefined % User can override this definition \def \NAMECITE #1#2{{\bf #1} \cite{#2}} \fi \NAMECITE{\#13753}{% Pritchard:1979:CPJ% }. \NAMECITE{$^*$}{% Damm:1983:SRH% }. \NAMECITE{$i$}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{$k$}{% Sousa:2016:CHL% }. \NAMECITE{$n$}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{-safety}{% Sousa:2016:CHL% }. \NAMECITE{-th}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{{0}}{% Horning:1989:BRE% }. \NAMECITE{{0-13-284027-8}}{% Horning:1989:BRE% }. \NAMECITE{{10}}{% Hoare:1971:CSI% }. \NAMECITE{11th}{% Kapur:1992:ADC,% Berghammer:2009:RKA,% Gibbons:2012:MPC% }. \NAMECITE{{14th}}{% Hofner:2014:RAM% }. \NAMECITE{16th}{% Abadi:2005:CCT% }. \NAMECITE{17th}{% IEEE:1976:ASF,% Hoare:1986:MPI% }. \NAMECITE{{18}}{% Pritchard:1979:CPJ% }. \NAMECITE{{1971}}{% Hoare:1971:CSI,% Hoare:1972:OST% }. \NAMECITE{{1980}}{% Hoare:2016:PST,% Hoare:2021:ATA% }. \NAMECITE{{1983}}{% ACM:1983:PFA% }. \NAMECITE{{1985}}{% Hoare:1986:MPI% }. \NAMECITE{{1991}}{% Gordon:1992:MRH% }. \NAMECITE{{1994}}{% Broy:1996:DPD% }. \NAMECITE{{1999}}{% Ryder:1999:PAS% }. \NAMECITE{{2.1}}{% Hoare:1966:LWM% }. \NAMECITE{{2.15s}}{% Hoare:1970:BRC% }. \NAMECITE{2/WG}{% Meyer:2008:VST% }. \NAMECITE{{2000}}{% Hoare:2001:ETS,% IEEE:2000:PSA% }. \NAMECITE{{2003}}{% Hoare:2004:RMN% }. \NAMECITE{{2007}}{% Muller:2010:ALS% }. \NAMECITE{{2007/2008}}{% Muller:2010:ALS% }. \NAMECITE{{2008}}{% Lenzerini:2008:PTS,% Muller:2010:ALS% }. \NAMECITE{{2011}}{% Hoare:2012:MT,% Hoare:2012:MTR% }. \NAMECITE{{2013}}{% Jones:2013:ICC% }. \NAMECITE{{20th}}{% Cipra:2000:BCE% }. \NAMECITE{{25}}{% VanGasteren:1990:CPD% }. \NAMECITE{{26th}}{% IEEE:2002:AIC% }. \NAMECITE{28/29}{% Broy:2001:PTC% }. \NAMECITE{{30}}{% Hoare:1987:CLP% }. \NAMECITE{33rd}{% Haddad:2012:ATP% }. \NAMECITE{{35}}{% Pettersson:1991:LEC% }. \NAMECITE{{3rd}}{% IEEE:1988:ASL% }. \NAMECITE{{4.20}}{% Barron:1975:BRS% }. \NAMECITE{{489}}{% Floyd:1975:AAA% }. \NAMECITE{{4th}}{% Wolff:2013:UTP% }. \NAMECITE{{56}}{% Pritchard:1979:CPJ% }. \NAMECITE{5th}{% Bottaci:2010:TAI% }. \NAMECITE{{63}}{% Hoare:1961:AP% }. \NAMECITE{{64}}{% Hoare:1961:AQ% }. \NAMECITE{{65}}{% Hoare:1961:AF% }. \NAMECITE{{68}}{% Hoare:1968:CA,% Hoare:1968:RDR,% Woodger:1969:MRA% }. \NAMECITE{6th}{% Berghammer:2009:RKA% }. \NAMECITE{70th}{% Liu:2013:TPF% }. \NAMECITE{75th}{% Jones:2011:DHC% }. \NAMECITE{'76}{% ACM:1976:SPE% }. \NAMECITE{7th}{% Ribeiro:2019:UTP% }. \NAMECITE{{8}}{% Horning:1989:BRE% }. \NAMECITE{85th}{% Ribeiro:2019:UTP% }. \NAMECITE{'90}{% Bjorner:1990:VVZ,% Baeten:1990:CTC,% Rishe:1990:PIC% }. \NAMECITE{'99}{% Ryder:1999:PAS% }. \NAMECITE{{A.}}{% Hoare:1968:LVW% }. \NAMECITE{{AADL}}{% Zhan:2019:UGC% }. \NAMECITE{Abrupt}{% Huisman:2000:JPV% }. \NAMECITE{Abstraction}{% Banerjee:2022:RPL% }. \NAMECITE{Abstractions}{% Jones:2021:FEA% }. \NAMECITE{Academic}{% Barron:1975:BRS,% Bottaci:2010:TAI% }. \NAMECITE{Acceptance}{% Enslow:1975:ILRa% }. \NAMECITE{Achievement}{% Hoare:2012:MT,% Black:2012:PSD,% Hoare:2012:MTR% }. \NAMECITE{ACM}{% ACM:1983:PFA,% Hoare:1987:CLP,% Hoare:2012:MT,% Hoare:2012:MTR,% Hoare:2016:PST,% Hoare:2021:ATA,% Lenzerini:2008:PTS,% Ryder:1999:PAS,% Ashenhurst:1987:ATA,% Floyd:1975:AAA,% Jones:2021:AI% }. \NAMECITE{Act}{% Hoare:2000:HAF% }. \NAMECITE{Ad}{% Wu:2019:USC% }. \NAMECITE{{Ada}}{% Feuer:1984:CAP% }. \NAMECITE{adaptation}{% Olderog:1983:NER% }. \NAMECITE{add}{% Hoare:1986:MAS% }. \NAMECITE{Addenda}{% Hoare:1974:ACA% }. \NAMECITE{Address}{% Hoare:1990:RAPb,% Hoare:1991:TCC,% Hoare:1978:SEK,% Hoare:1990:LMM,% Hoare:1997:UTC% }. \NAMECITE{addressing}{% Hoare:1965:NIA% }. \NAMECITE{adjunctions}{% Martin:1991:PAO% }. \NAMECITE{Advanced}{% Broy:1996:DPD,% Muller:2010:ALS% }. \NAMECITE{Afternoon}{% Dijkstra:1982:PTP% }. \NAMECITE{Ago}{% McReynolds:1997:LBS% }. \NAMECITE{Aided}{% Barthe:2012:PRH% }. \NAMECITE{AKA}{% Berghammer:2009:RKA% }. \NAMECITE{Algebra}{% Brookes:2021:CPP,% Hayes:2019:DAR,% Hoare:1992:AM,% Hoare:1993:AMa,% Hoare:1993:AMb,% Hoare:1995:AM,% Hoare:1996:AM,% Hoare:2005:PAUa,% Hoare:2005:PAUb,% Hoare:2019:CST,% Seres:1999:ALP,% Struth:2021:THA,% vanStaden:2013:AUO,% Berghammer:2009:RKA,% Groote:1994:PAG,% He:1993:AOS,% Hoare:1990:RAPa,% Hoare:1990:RAPb,% Hoare:1992:RAP,% Hoare:2009:CKA,% Hoare:2009:FCK,% Hoare:2011:CKA,% Hoare:2012:PA,% Hoare:2014:DCK,% Hoare:2016:DCK,% Hoare:2019:CSTa,% Kozen:2000:HLK% }. \NAMECITE{Algebraic}{% Aichernig:2019:TPA,% Gardiner:1995:APC,% He:1987:ASP,% Hoare:1986:ASP,% Hoare:1987:ASP,% Hoare:1991:ASP,% Hoare:1994:ACO,% Hoare:1997:ADO,% Hoare:2000:ADO,% Hofner:2014:RAM,% Delbianco:2013:HSR,% Gritzner:1996:RAM,% Hoare:1990:AAV% }. \NAMECITE{Algebras}{% Broy:2003:MAL,% Butterfield:2019:IOA% }. \NAMECITE{ALGOL}{% Wirth:1966:ECD,% Hoare:1962:REA,% Hoare:1963:EAI,% Hoare:1964:EAP,% Hoare:1968:CA,% Hoare:1968:RDR,% Wirth:1966:CDA,% Woodger:1969:MRA,% Hoare:1964:BRA% }. \NAMECITE{Algorithm}{% Brown:1976:RAA,% Floyd:1975:AAA,% Grubel:1996:ADT,% Grubel:1998:HSA,% Kirschenhofer:1998:CHF,% He:1987:ASP,% Neuhold:1977:UHM,% Pritchard:1979:CPJ,% Prodinger:1995:MQH,% VanGasteren:1990:CPD,% Verjus:1987:PDA,% Brown:1976:RAA,% Hoare:1961:AF,% Hoare:1961:AP,% Hoare:1961:AQ% }. \NAMECITE{Algorithms}{% Cipra:2000:BCE,% vanDiepen:1986:PDT,% denHartog:2008:TMC% }. \NAMECITE{Always}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{Always-true}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{Ambiguities}{% Welsh:1977:AIP% }. \NAMECITE{{Amir}}{% Manna:2010:TVE% }. \NAMECITE{amp}{% Hoare:2004:AA% }. \NAMECITE{analysing}{% Nielson:1987:HLP% }. \NAMECITE{Analysis}{% Fouz:2012:SAQ,% Hoare:1961:MSS,% Rehof:2010:ADS% }. \NAMECITE{Annual}{% IEEE:1988:ASL,% IEEE:2002:AIC,% ACM:1976:SPE,% ACM:1983:PFA,% IEEE:1976:ASF% }. \NAMECITE{Answer}{% Lewis:1997:BCI,% Thielecke:2006:FRA% }. \NAMECITE{Antony}{% Black:2012:PSD,% Davies:2000:MPC,% Dijkstra:1999:FWT,% Frana:2002:ICA% }. \NAMECITE{application}{% Hoare:1976:CST,% Haddad:2012:ATP% }. \NAMECITE{Applications}{% Berghammer:2009:RKA,% Elliott:1989:SAM,% Herbert:2004:CST,% IEEE:2002:AIC,% Hoare:2010:MJD,% Rishe:1990:PIC% }. \NAMECITE{applied}{% Hoare:1988:PCC% }. \NAMECITE{Approach}{% Grubel:1998:HSA,% Hoare:1989:NAC,% Hoare:1993:NFA,% Hoare:2005:PAUa,% Hoare:2005:PAUb,% Hoare:1971:PPA,% Hoare:1975:PPA,% Hoare:1976:PPA,% Hoare:1990:AAV,% Hortala-Gonzalez:1989:HLN,% Ridge:2009:VDS% }. \NAMECITE{approaches}{% Bruni:2005:CTA% }. \NAMECITE{April}{% ACM:1983:PFA,% Bjorner:1990:VVZ,% Hofner:2014:RAM% }. \NAMECITE{APSEC}{% IEEE:2000:PSA% }. \NAMECITE{architectures}{% Rishe:1990:PIC% }. \NAMECITE{arithmetic}{% Bergstra:1983:HLP% }. \NAMECITE{Art}{% Bates:1976:SPI% }. \NAMECITE{Asia}{% IEEE:2000:PSA% }. \NAMECITE{Asia-Pacific}{% IEEE:2000:PSA% }. \NAMECITE{assembly}{% Ni:2006:CAP% }. \NAMECITE{assertion}{% Chisholm:1989:ARP% }. \NAMECITE{Assertional}{% Pettersson:1991:LEC,% Shankar:1993:IAR% }. \NAMECITE{Assertions}{% Hoare:2000:A,% Hoare:2002:AMS,% Hoare:2002:APP,% Hoare:2002:APS,% Hoare:2002:APV,% Hoare:2003:A,% Hoare:2003:APP% }. \NAMECITE{Assessing}{% Apt:2021:ASI,% Feuer:1984:CAP% }. \NAMECITE{associated}{% Chisholm:1989:ARP% }. \NAMECITE{Asymptotic}{% Grubel:1996:ADT% }. \NAMECITE{asynchronous}{% Josephs:1989:TAP% }. \NAMECITE{asynchronously}{% deBoer:2002:HLD% }. \NAMECITE{asynchrony}{% He:1990:TSA% }. \NAMECITE{Atlanta}{% Ryder:1999:PAS% }. \NAMECITE{atom}{% Hoare:2004:AA% }. \NAMECITE{atomic}{% Wing:1989:VAD% }. \NAMECITE{Aug}{% Ershov:1974:IST% }. \NAMECITE{August}{% Abadi:2005:CCT,% Bauer:1976:LHI,% Broy:1996:DPD,% Hoare:1972:OST,% Hoare:2001:ETS,% IEEE:2002:AIC,% Wolff:2013:UTP,% Dijkstra:1970:LPC% }. \NAMECITE{Author}{% Jones:2021:ABI% }. \NAMECITE{authorization}{% Becker:2010:LSM% }. \NAMECITE{Automated}{% Boyer:1992:ACP,% Boyer:1996:APO,% Kapur:1992:ADC,% Sokolowski:1987:SHL,% Chisholm:1989:ARP,% Kapur:1992:ADC% }. \NAMECITE{automorphisms}{% Hoare:1979:CGW% }. \NAMECITE{Auxiliary}{% Kleymann:1999:HLA,% vonOheimb:2002:HLN% }. \NAMECITE{Award}{% Ashenhurst:1987:ATA,% Hoare:2016:PST,% Hoare:2021:ATA,% Black:2012:PSD,% Hoare:2012:MTR,% Hoare:2012:MT% }. \NAMECITE{Axiom}{% Clarke:1979:PLC,% Qian:1990:ASD% }. \NAMECITE{Axiomatic}{% Bergstra:1984:ASP,% Hoare:1969:ABC,% Hoare:1972:ADP,% Hoare:1973:ADP,% Hoare:1974:ACA,% Hoare:1983:ABC,% Hoare:2001:ABC,% Hoare:2002:ABC,% Hoare:1971:PPA,% Hoare:1974:ADP,% Hoare:1975:PPA,% Hoare:1976:PPA,% Hoare:1996:PAB,% Hoare:1996:PPA,% Hoare:2009:VRA% }. \NAMECITE{Axiomatics}{% Cherniavsky:1979:CCH% }. \NAMECITE{{Axiomatization}}{% denHartog:2008:TMC% }. \NAMECITE{Axiomatizations}{% Clarke:1983:EAH% }. \NAMECITE{B}{% Horning:1989:BRE% }. \NAMECITE{Based}{% Bergstra:1984:ASP,% Kaubisch:1982:DES,% Olderog:1981:SCH,% Barthe:2009:FCC% }. \NAMECITE{basic}{% Bowen:1996:PIP% }. \NAMECITE{Basis}{% Hoare:1961:MSS,% Hoare:1969:ABC,% Hoare:1983:ABC,% Hoare:2001:ABC,% Hoare:2002:ABC,% Hoare:1981:TMB,% Hoare:1996:PAB,% Hoare:2009:VRA% }. \NAMECITE{Bazilevskii}{% Baer:1965:RPP% }. \NAMECITE{BC}{% Lenzerini:2008:PTS% }. \NAMECITE{be}{% Page:1989:SME% }. \NAMECITE{Beach}{% Rishe:1990:PIC% }. \NAMECITE{Beauty}{% Feijen:1990:BOB% }. \NAMECITE{bedrock}{% Chlipala:2013:BSP% }. \NAMECITE{before}{% Hoare:1971:CSI,% Hoare:1986:MPI% }. \NAMECITE{Behaviour}{% Hoare:2012:NMC% }. \NAMECITE{behind}{% Hoare:1973:HLP% }. \NAMECITE{being}{% Dijkstra:1982:PTP% }. \NAMECITE{Belfast}{% Hoare:1972:OST,% Hoare:1971:CSI,% Sufrin:2021:TBO% }. \NAMECITE{Best}{% Cipra:2000:BCE% }. \NAMECITE{better}{% Hoare:1972:PBP% }. \NAMECITE{Binary}{% Lewis:1997:BCI% }. \NAMECITE{Biographies}{% Jones:2021:ABI,% Weiss:1988:BOP% }. \NAMECITE{Biographies/Index}{% Jones:2021:ABI% }. \NAMECITE{Birthday}{% Feijen:1990:BOB,% Jones:2011:DHC,% Liu:2013:TPF,% Ribeiro:2019:UTP% }. \NAMECITE{Blocks}{% Hoare:2011:RB% }. \NAMECITE{Bonn}{% Broy:2001:PTC% }. \NAMECITE{Book}{% Anonymous:1987:BRC,% Barron:1975:BRS,% Barth:1974:BRJ,% Hoare:1963:BR,% Hoare:1964:BRA,% Hoare:1970:BR,% Hoare:1970:BRC,% Hoare:1977:BR,% Horning:1989:BRE,% Lloyd:1974:BRS,% Brockhaus:1973:BRC% }. \NAMECITE{Boston}{% ACM:1983:PFA% }. \NAMECITE{Bottom}{% Hoare:1999:TPT% }. \NAMECITE{Bottom-Up}{% Hoare:1999:TPT% }. \NAMECITE{{Brian}}{% Jones:2011:DHC% }. \NAMECITE{Broadcasting}{% Broy:1988:BBC% }. \NAMECITE{{Brooks}}{% McReynolds:1997:LBS% }. \NAMECITE{Buffering}{% Broy:1988:BBC% }. \NAMECITE{Business}{% Feijen:1990:BOB% }. \NAMECITE{Butterworths}{% Hoare:1970:BRC% }. \NAMECITE{C}{% Anonymous:1987:BRC,% Baer:1965:RPP,% Barron:1975:BRS,% Barth:1974:BRJ,% Brockhaus:1973:BRC,% Hoare:1970:BRC,% Horning:1989:BRE,% Lloyd:1974:BRS,% Roscoe:1994:CME,% Feuer:1984:CAP,% Hoare:1988:PCC,% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb,% Olsen:1997:LWJ% }. \NAMECITE{{C-MOS}}{% Hoare:1988:PCC,% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb% }. \NAMECITE{{C.}}{% Ashcroft:1976:RPP,% Dijkstra:1970:LPC,% Dijkstra:1974:LCR,% Dijkstra:1975:VTO,% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa,% Dijkstra:1982:PTP,% Dijkstra:1982:VTO,% Dijkstra:20xx:ERC,% Hoare:1982:VTO,% Jones:2010:RWC,% Shustek:2009:IIC% }. \NAMECITE{CA}{% Abadi:2005:CCT% }. \NAMECITE{CADE}{% Kapur:1992:ADC% }. \NAMECITE{CADE-11}{% Kapur:1992:ADC% }. \NAMECITE{Calculi}{% Hoare:2012:LPU,% Olderog:1981:SCH,% vanStaden:2013:AUO,% Hoare:2014:LPU,% Kirkerud:1982:CHC% }. \NAMECITE{Calculus}{% Hoare:1981:CTCb,% Hoare:2019:CST,% Reus:2001:HCV,% Wu:2019:USC,% Hoare:1981:CTCa,% Hoare:1982:CCT,% Hoare:1985:CNP,% Hoare:2019:CSTa,% Milner:1990:IOC,% Zhou:1991:CD,% vonKarger:1995:SC% }. \NAMECITE{Call}{% deBoer:2021:CCR% }. \NAMECITE{Call-by-Value}{% deBoer:2021:CCR% }. \NAMECITE{Calls}{% BrinchHansen:2002:OCP,% Shaner:2007:MVH% }. \NAMECITE{can}{% Page:1989:SME% }. \NAMECITE{Canada}{% Lenzerini:2008:PTS% }. \NAMECITE{Card}{% Hoare:2010:UCT% }. \NAMECITE{{Cartesian}}{% Sousa:2016:CHL% }. \NAMECITE{Case}{% Hoare:1964:CE% }. \NAMECITE{Categorical}{% He:1990:CSP,% Hoare:1990:CSP,% Knijnenburg:1992:CIP,% He:1990:DRC,% Hoare:1990:DRC% }. \NAMECITE{categories}{% Martin:1991:PAO% }. \NAMECITE{Category}{% Hoare:1989:NAC% }. \NAMECITE{Causality}{% Hoare:2019:CST,% Hoare:2019:CSTa% }. \NAMECITE{causally}{% Stoller:1995:VPU% }. \NAMECITE{causally-ordered}{% Stoller:1995:VPU% }. \NAMECITE{CBE}{% Hoare:2004:RMN% }. \NAMECITE{{CCS}}{% He:2010:CRC% }. \NAMECITE{{CE}}{% Gozum:1997:LWC% }. \NAMECITE{{Century}}{% Cipra:2000:BCE% }. \NAMECITE{certification}{% Barthe:2009:FCC% }. \NAMECITE{Certified}{% Cai:2007:CSM,% Ni:2006:CAP% }. \NAMECITE{Certifying}{% Chajed:2017:CFS% }. \NAMECITE{Chain}{% Grubel:1998:HSA% }. \NAMECITE{Challenge}{% Hoare:1996:UTC,% Hoare:2003:VCGa,% Hoare:2008:VST,% Hoare:2003:VCGb,% Hoare:2005:VCG,% Woodcock:2021:VGC% }. \NAMECITE{Challenges}{% Hayes:2019:DAR,% Hoare:2004:GCC,% Hoare:2005:GCC% }. \NAMECITE{Characterisation}{% Hoare:1994:ACO% }. \NAMECITE{characterization}{% Olderog:1983:CHL% }. \NAMECITE{characterizations}{% Makowsky:1989:WSO% }. \NAMECITE{Charles}{% Black:2012:PSD,% Dijkstra:1999:FWT,% Frana:2002:ICA% }. \NAMECITE{chief}{% Hoare:1970:BRC% }. \NAMECITE{circuit}{% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb% }. \NAMECITE{circuits}{% Hoare:1988:PCC,% Hoare:1990:MSS,% Zhou:1992:MSS% }. \NAMECITE{{CKA}}{% Moller:2015:EIM% }. \NAMECITE{claims}{% Chisholm:1989:ARP% }. \NAMECITE{class}{% Dijkstra:20xx:ERC% }. \NAMECITE{Classical}{% Feng:2021:QHL,% Roscoe:1994:CME% }. \NAMECITE{{Clint}}{% Ashcroft:1976:RPP% }. \NAMECITE{Closing}{% Hoare:1994:HSCa,% Hoare:1994:HSCb% }. \NAMECITE{Clothes}{% Hoare:1981:EOC,% Hoare:1987:EOC% }. \NAMECITE{{Club}}{% Dijkstra:1982:PTP% }. \NAMECITE{Co}{% Zhan:2019:UGC% }. \NAMECITE{Co-modelling}{% Zhan:2019:UGC% }. \NAMECITE{code}{% Barthe:2009:FCC,% Boyer:1992:ACP,% Boyer:1996:APO,% Cai:2007:CSM,% Hoare:2000:LC,% Ni:2006:CAP,% Thielecke:2006:FRA% }. \NAMECITE{code-based}{% Barthe:2009:FCC% }. \NAMECITE{{Coded}}{% Sun:1996:TRH% }. \NAMECITE{Coinitial}{% Hoare:1979:CGW% }. \NAMECITE{collection}{% Hoare:1974:OSS% }. \NAMECITE{College}{% Jones:2013:ICC% }. \NAMECITE{Collusion}{% Hoare:2007:SEC% }. \NAMECITE{combinational}{% Hoare:1991:TDCa,% Hoare:1991:TDCb% }. \NAMECITE{Combining}{% Groote:1994:PAG,% Chlipala:2013:BSP% }. \NAMECITE{Comm}{% Hoare:1987:CLP% }. \NAMECITE{Command}{% Enslow:1975:ILRc,% Hoare:1975:HDP,% Hoare:1976:HDP% }. \NAMECITE{Comments}{% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Pettersson:1991:LEC,% Pritchard:1979:CPJ,% VanGasteren:1990:CPD% }. \NAMECITE{commercial}{% Boyer:1992:ACP% }. \NAMECITE{Communicating}{% Brookes:1984:TCS,% Hoare:1978:CCS,% Hoare:1978:CSPa,% Hoare:1978:CSPb,% Hoare:1981:CTCb,% Hoare:1981:PCC,% Hoare:1985:CSP,% Hoare:1986:NCS,% Hoare:1987:ASP,% Hoare:2002:CSP,% Hoare:2008:SLS,% Hoare:2021:CSP,% Kaubisch:1982:DES,% Olderog:1986:SOS,% Enikeev:1987:MTC,% Hehner:1983:MCM,% Hoare:1980:MCSa,% Hoare:1980:MCSb,% Hoare:1981:CTCa,% Hoare:1981:MCS,% Hoare:1982:CCT,% Hoare:1983:NCS,% Hoare:1985:NCS,% Hoare:1991:ASP,% Olderog:1983:SOS,% Zhou:1981:PCC,% deBoer:2002:HLD,% Abdallah:2005:CSP,% Hoare:1983:CSP,% Anonymous:1987:BRC% }. \NAMECITE{Communication}{% Broy:1988:BBC,% Hoare:1991:DCC,% Silberschatz:1981:PDC,% Francez:1978:SNC,% Francez:1979:SNC% }. \NAMECITE{communications}{% Hoare:1993:WSE% }. \NAMECITE{commute}{% Flannery:1990:HSP% }. \NAMECITE{Comparing}{% Bruni:2005:CTA,% Feuer:1984:CAP% }. \NAMECITE{Comparisons}{% Kirschenhofer:1998:CHF% }. \NAMECITE{Compensable}{% Hoare:2007:CT,% Hoare:2010:CT,% Bruni:2005:CTA% }. \NAMECITE{compilation}{% Hoare:1966:SPC,% Hoare:1992:RAP% }. \NAMECITE{Compiler}{% Hoare:1993:NFA,% Hoare:2003:TVC,% Hoare:2003:VCGa,% Hoare:2004:TVC,% Bicarregui:2006:VSR,% Hoare:2003:VC,% Hoare:2003:VCGb,% Hoare:2005:VCG% }. \NAMECITE{compiling}{% Hoare:1990:AAV,% Hoare:1990:RAPa,% Hoare:1990:RAPb% }. \NAMECITE{Complementary}{% Hoare:1974:CCF% }. \NAMECITE{Complete}{% Cherniavsky:1979:CCH,% Damm:1983:SRH,% Olderog:1981:SCH,% Arthan:2009:GFS,% Hehner:1983:MCM% }. \NAMECITE{Completeness}{% Bergstra:1982:TTA,% Kirkerud:1982:CHC,% Xu:2016:CHL,% deBoer:2021:CCR,% Bergstra:1982:ECH,% Gardiner:1995:APC,% RodriguezArtalejo:1985:SQA% }. \NAMECITE{Complexity}{% Hoare:1993:MPM,% deBoer:2021:CCR,% Cohen:2000:NCP% }. \NAMECITE{composition}{% Bruni:2005:CTA,% Flannery:1990:HSP% }. \NAMECITE{Compositional}{% Hooman:1992:CVR,% DeBoer:1997:HSC,% Saabas:2007:CNS% }. \NAMECITE{computable}{% Blass:2001:ICL% }. \NAMECITE{computation}{% Jacobs:2015:DHM,% Nielson:1987:HLP% }. \NAMECITE{Computations}{% Guttmann:2019:CFC% }. \NAMECITE{Computer}{% Barthe:2012:PRH,% Herbert:2004:CST,% Hoare:1969:ABC,% Hoare:1971:CSI,% Hoare:1973:CPE,% Hoare:1976:CST,% Hoare:1983:ABC,% Hoare:1989:NAC,% Hoare:2001:ABC,% Hoare:2001:ETS,% Hoare:2002:ABC,% Hofner:2014:RAM,% IEEE:1976:ASF,% IEEE:1988:ASL,% IEEE:2002:AIC,% Berghammer:2009:RKA,% Davies:2000:MPC,% Hoare:1981:TMB,% Hoare:1986:MAS,% Hoare:1989:FMC,% Hoare:1996:PAB,% Hoare:2009:VRA,% Hoare:2007:IPC,% Hoare:1970:BRC% }. \NAMECITE{Computer-Aided}{% Barthe:2012:PRH% }. \NAMECITE{Computing}{% ACM:1983:PFA,% Dijkstra:1982:SWC,% Hoare:1989:ECS,% Hoare:1996:UTC,% Hoare:2003:VCGa,% Hoare:2004:GCC,% Hoare:2005:GCC,% Jones:2011:DHC,% Jones:2013:ICC,% Pritchard:1979:CPJ,% Anonymous:1976:SSE,% Hoare:1996:MMC,% Hoare:1998:SCE,% Hoare:2003:KTK,% Hoare:2003:VCGb,% Hoare:2005:VCG,% Horning:1989:BRE,% ACM:1976:SPE% }. \NAMECITE{Concept}{% Hoare:1974:MOS,% Hoare:2002:MOS% }. \NAMECITE{CONCUR}{% Abadi:2005:CCT,% Abadi:2005:CCT,% Baeten:1990:CTC% }. \NAMECITE{Concurrency}{% Baeten:1990:CTC,% Butterfield:2019:IOA,% Hayes:2019:DAR,% Hoare:1991:DCC,% Hoare:2010:FGCa,% Struth:2021:THA,% Abadi:2005:CCT,% Cleaveland:1996:SDC,% DeBoer:1997:HSC,% Francez:1978:SNC,% Francez:1979:SNC,% He:2005:LTC,% Hoare:1990:TCC,% Hoare:1991:TCC,% Hoare:1997:UTC,% Hoare:2010:FGCb,% Hoare:2013:LPC,% Turon:2013:URH% }. \NAMECITE{Concurrent}{% BrinchHansen:2002:OCP,% Hoare:2009:CKA,% Hoare:2011:CKA,% Hoare:2012:NMC,% Lamport:1980:HLC,% Shankar:1993:IAR,% Hoare:2008:VFG,% Hoare:2009:FCK,% Hoare:2011:LEL,% Hoare:2013:USC,% Hoare:2014:DCK,% Hoare:2014:LCP,% Hoare:2016:DCK,% Milner:1990:IOC,% Sergey:2016:HSS,% Shapiro:2006:PPC,% Stirling:1988:GOG,% Vafeiadis:2006:PCH% }. \NAMECITE{condition}{% He:2000:UTH,% Homeier:1995:MVV% }. \NAMECITE{conditions}{% Sergey:2016:HSS% }. \NAMECITE{Conference}{% Abadi:2005:CCT,% Berghammer:2009:RKA,% Bottaci:2010:TAI,% Broy:2001:PTC,% Gibbons:2012:MPC,% Haddad:2012:ATP,% Hofner:2014:RAM,% IEEE:2000:PSA,% IEEE:2002:AIC,% Kapur:1992:ADC,% Meyer:2008:VST,% Ryder:1999:PAS,% Anonymous:1976:SSE,% Rishe:1990:PIC% }. \NAMECITE{conformance}{% Fournet:2004:SFC% }. \NAMECITE{conjunction}{% Hoare:1990:TCC,% Hoare:1991:TCC% }. \NAMECITE{Connecting}{% Guttmann:2019:CFC% }. \NAMECITE{conservation}{% Hoare:1973:GCL% }. \NAMECITE{considerations}{% Pratt:1976:SCF% }. \NAMECITE{consistency}{% Gardiner:1995:APC,% Hoare:1982:CCT% }. \NAMECITE{Consistent}{% Cherniavsky:1979:CCH,% Hoare:1974:CCF% }. \NAMECITE{Constrained}{% Reus:2001:HCV% }. \NAMECITE{Construction}{% Hoare:2001:ETS,% Gibbons:2012:MPC,% vanAmmers:1998:PCC% }. \NAMECITE{constructors}{% Flannery:1990:HSP% }. \NAMECITE{Constructs}{% Clarke:1979:PLC% }. \NAMECITE{context}{% vanAmmers:1998:PCC% }. \NAMECITE{Continuations}{% Tennent:1991:CPW,% Delbianco:2013:HSR% }. \NAMECITE{Contradiction}{% Hoare:1978:ESS% }. \NAMECITE{Contribution}{% Wirth:1966:CDA,% Wirth:1966:ECD% }. \NAMECITE{Contributions}{% Broy:2001:PTC,% Broy:2002:SPC,% Broy:2001:PTC% }. \NAMECITE{Control}{% Enslow:1975:ILRc,% Hoare:1993:MPM,% Hoare:1975:HDP,% Hoare:1976:HDP% }. \NAMECITE{conversation}{% Dale:1994:CST% }. \NAMECITE{Copy}{% Olderog:1981:SCH% }. \NAMECITE{Copying}{% vanDiepen:1986:PDT% }. \NAMECITE{Correct}{% He:1994:PCS% }. \NAMECITE{Correctness}{% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Hoare:1981:CTCb,% Hoare:1981:PCC,% Hoare:2001:PCD,% Hoare:2002:PCD,% Hoare:2007:IPC,% Olderog:1984:CPP,% Boyer:1992:ACP,% Chajed:2017:CFS,% Fokkinga:1987:CPS,% Gritzner:1996:RAM,% Hoare:1972:PCD,% Hoare:1975:PCP,% Hoare:1976:PCD,% Hoare:1981:CTCa,% Hoare:1982:CCT,% Hoare:1988:PCC,% Hoare:1990:MSS,% Hoare:1990:RAPa,% Hoare:1990:RAPb,% Hoare:1992:RAP,% Hoare:1996:PPC,% Sergey:2016:HSS,% Vafeiadis:2006:PCH,% Zhou:1981:PCC,% Zhou:1992:MSS,% denHartog:2008:TMC% }. \NAMECITE{Corrigenda}{% Hoare:1974:ACA,% Hoare:1987:CLP% }. \NAMECITE{Corrigendum}{% Hoare:1978:CCS% }. \NAMECITE{cost}{% Hoare:1976:HCP% }. \NAMECITE{couple}{% Hoare:1985:CNP% }. \NAMECITE{courses}{% Hoare:1976:SPI% }. \NAMECITE{{Crash}}{% Chajed:2017:CFS% }. \NAMECITE{crashes}{% Chajed:2017:CFS% }. \NAMECITE{Critic}{% Lewis:1997:BCI% }. \NAMECITE{Critique}{% Greif:1981:SSW,% Hoare:1968:CA,% ODonnell:1982:CFH% }. \NAMECITE{cryptographic}{% Barthe:2009:FCC,% denHartog:2008:TMC% }. \NAMECITE{CSP}{% Abdallah:2005:CSP,% Brookes:2021:CPP,% He:2010:CRC,% Hoare:1985:SSN,% Hoare:2006:WEC,% Lamport:1984:HLC,% May:2021:COI,% Sridhar:1985:JEC% }. \NAMECITE{Cultures}{% Hoare:2007:SEC% }. \NAMECITE{{CV}}{% Misra:2021:C% }. \NAMECITE{Cyber}{% Zhan:2019:UGC% }. \NAMECITE{Cyber-Physical}{% Zhan:2019:UGC% }. \NAMECITE{Cyclic}{% Brotherston:2008:CPP% }. \NAMECITE{{D.}}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{Dahl}{% Barron:1975:BRS,% Barth:1974:BRJ,% Lloyd:1974:BRS,% Owe:2004:OOF% }. \NAMECITE{Data}{% Banerjee:2022:RPL,% He:1986:DRR,% He:1990:DRC,% Hoare:1968:DST,% Hoare:1975:DR,% Hoare:1990:DRC,% Hoare:2001:PCD,% Hoare:2002:PCD,% Bergstra:1984:HLP,% Hoare:1972:NDS,% Hoare:1972:PCD,% Hoare:1975:RDS,% Hoare:1976:PCD,% Hoare:1987:PDR,% Hoare:1996:PPC,% Hoare:2011:UMD,% LeGuyadec:1996:SLP,% Wing:1989:VAD% }. \NAMECITE{data-parallel}{% LeGuyadec:1996:SLP% }. \NAMECITE{Database}{% Lenzerini:2008:PTS,% Qian:1990:ASD% }. \NAMECITE{databases}{% Rishe:1990:PIC% }. \NAMECITE{Dawn}{% Daylight:2012:DSE% }. \NAMECITE{Deadlocks}{% Struble:1997:LDJ% }. \NAMECITE{decidable}{% Bergstra:1982:SNS% }. \NAMECITE{Decisions}{% Hayes:2019:DAR% }. \NAMECITE{decomposition}{% Takaoka:1987:DRH% }. \NAMECITE{Dedicated}{% Jones:2011:DHC,% Liu:2013:TPF,% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa,% Dijkstra:1999:FWT,% Ribeiro:2019:UTP,% Dijkstra:1982:PTP% }. \NAMECITE{deduction}{% Kapur:1992:ADC% }. \NAMECITE{Deductive}{% Broy:1996:DPD% }. \NAMECITE{Definition}{% Hoare:1972:ADP,% Hoare:1973:ADP,% Hoare:1974:ACA,% Hoare:1974:ADP,% Hoare:1996:PPA% }. \NAMECITE{delivered}{% Hoare:1971:CSI,% Hoare:1986:MPI% }. \NAMECITE{Denotational}{% Aichernig:2019:TPA% }. \NAMECITE{Dependable}{% Jones:2011:DHC% }. \NAMECITE{dependent}{% Nanevski:2008:YDT% }. \NAMECITE{Derivation}{% vanDiepen:1986:PDT,% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb,% Hoare:1997:ADO,% Hoare:2000:ADO% }. \NAMECITE{described}{% Page:1989:SME% }. \NAMECITE{Design}{% Enslow:1975:ILRb,% Hayes:2019:DAR,% Hoare:1973:HPLa,% Hoare:1973:HPLb,% Hoare:1973:HPLc,% Hoare:1987:DPM,% Hoare:1987:OSF,% Hoare:1991:DPM,% Hoare:1993:NFA,% Reus:2001:HCV,% Ryder:1999:PAS,% Broy:1996:DPD,% Gordon:1992:MRH,% Hoare:1974:HPL,% Hoare:1974:SDP,% Hoare:1975:HDP,% Hoare:1976:HDP,% Hoare:1989:FMC,% Hoare:1996:LED,% Hoare:2010:MJD% }. \NAMECITE{designs}{% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb% }. \NAMECITE{determinism}{% Hoare:1980:TND% }. \NAMECITE{Deterministic}{% Mamouras:2016:HLD,% deBoer:2002:HLD% }. \NAMECITE{Developing}{% Hayes:2019:DAR% }. \NAMECITE{Development}{% Wirth:1966:CDA,% Wirth:1966:ECD,% Bjorner:1990:VVZ% }. \NAMECITE{Developments}{% Hoare:1991:DCC,% Hoare:2014:DCK,% Hoare:2016:DCK% }. \NAMECITE{dialog}{% Enikeev:1987:MTC% }. \NAMECITE{did}{% Hoare:1996:HDS% }. \NAMECITE{Dijkstra}{% Barron:1975:BRS,% Barth:1974:BRJ,% Lloyd:1974:BRS,% Apt:2022:EWD,% Boyer:2002:MEW,% Daylight:2012:DSE,% Feijen:1990:BOB,% Hoare:2003:EWD,% Jacobs:2015:DHM% }. \NAMECITE{Directed}{% Silberschatz:1981:PDC% }. \NAMECITE{directions}{% Cleaveland:1996:SDC% }. \NAMECITE{discipline}{% Dijkstra:1976:DP,% Hoare:1973:CPE% }. \NAMECITE{disciplines}{% Hoare:1973:GCL% }. \NAMECITE{Discrete}{% Kaubisch:1982:DES% }. \NAMECITE{Discussion}{% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Gordon:1992:MRH% }. \NAMECITE{{Discussions}}{% Meyer:2008:VST% }. \NAMECITE{Distinguished}{% Hoare:2012:MT,% Black:2012:PSD,% Hoare:2012:MTR% }. \NAMECITE{Distributed}{% Joseph:1987:PRF,% He:1987:ASP,% Mancini:1988:HLD,% Rehof:2010:ADS,% Ridge:2009:VDS,% VanGasteren:1990:CPD,% Verjus:1987:PDA% }. \NAMECITE{Distribution}{% Grubel:1996:ADT% }. \NAMECITE{Doctoral}{% Jones:2021:DS% }. \NAMECITE{does}{% Hoare:2004:YWT% }. \NAMECITE{Doha}{% Berghammer:2009:RKA% }. \NAMECITE{{DOM}}{% Gardner:2008:LHR% }. \NAMECITE{domain}{% Flannery:1990:HSP% }. \NAMECITE{Down}{% Hoare:1999:TPT,% Olsen:1997:LWJ% }. \NAMECITE{Draft}{% Hoare:1968:RDR,% Woodger:1969:MRA% }. \NAMECITE{{DSE}}{% Hoare:2004:EHDa,% Hoare:2004:EHDb% }. \NAMECITE{durations}{% Zhou:1991:CD% }. \NAMECITE{Dynamic}{% Banerjee:2022:RPL,% deBoer:2002:HLD% }. \NAMECITE{{E.}}{% Pritchard:1979:CPJ% }. \NAMECITE{ed}{% Horning:1989:BRE% }. \NAMECITE{Edinburgh}{% IEEE:1988:ASL% }. \NAMECITE{Editor}{% Pettersson:1991:LEC,% Welch:1997:LEI% }. \NAMECITE{Editorial}{% Hoare:1972:GEQ,% Hoare:1994:GE% }. \NAMECITE{Editors}{% Cipra:2000:BCE% }. \NAMECITE{{Edsger}}{% Apt:2022:EWD,% Boyer:2002:MEW,% Feijen:1990:BOB,% Hoare:2003:EWD,% Hoare:2022:FYE% }. \NAMECITE{Effective}{% Clarke:1983:EAH,% Jones:2021:FEA% }. \NAMECITE{Effects}{% vonOheimb:2002:HLN% }. \NAMECITE{Efficient}{% Johnston:1975:MRE% }. \NAMECITE{eighth}{% ACM:1976:SPE% }. \NAMECITE{elected}{% Dijkstra:1982:PTP% }. \NAMECITE{Elements}{% Brown:1976:RAA,% Floyd:1975:AAA,% Prodinger:1995:MQH% }. \NAMECITE{{Elliott}}{% Hoare:1962:REA,% Hoare:1963:EAI,% Hoare:1964:EAP% }. \NAMECITE{embedded}{% Ni:2006:CAP% }. \NAMECITE{Emeritus}{% Anonymous:20xx:THE% }. \NAMECITE{emperor}{% Hoare:1987:EOC,% Hoare:1981:EOC% }. \NAMECITE{Engeering}{% IEEE:2000:PSA% }. \NAMECITE{Engineering}{% Beckert:2006:ISF,% Broy:2001:PTC,% Broy:2002:SPC,% Broy:2003:MAL,% Broy:2005:ETS,% Daylight:2012:DSE,% Hoare:1978:ESS,% Hoare:2001:ETS,% Hoare:2002:APS,% Hoare:2007:SEC,% Anonymous:1976:SSE,% Hoare:1973:CPE,% Hoare:1975:SE,% Hoare:1978:SEK,% Hoare:1983:PEP,% Hoare:1993:WSE,% Hoare:1996:LED,% Hoare:1998:SCE,% Hoare:2002:AMS,% Muller:2010:ALS% }. \NAMECITE{{England}}{% IEEE:2002:AIC% }. \NAMECITE{enriched}{% Martin:1991:PAO% }. \NAMECITE{Envoi}{% Hoare:2021:E% }. \NAMECITE{{Eratosthenes}}{% Hoare:1972:PSP% }. \NAMECITE{Errata}{% Wirth:1966:ECD% }. \NAMECITE{{Esprit}}{% Bowen:1996:PIP% }. \NAMECITE{Essays}{% Hoare:1989:ECS,% Jones:2011:DHC,% Liu:2013:TPF,% Manna:2010:TVE,% Owe:2004:OOF,% Roscoe:1994:CME,% Horning:1989:BRE% }. \NAMECITE{EUROCOMP}{% Anonymous:1976:SSE% }. \NAMECITE{Europe}{% Bjorner:1990:VVZ% }. \NAMECITE{European}{% Anonymous:1976:SSE% }. \NAMECITE{Event}{% Kaubisch:1982:DES% }. \NAMECITE{ever}{% Hoare:2006:WEC% }. \NAMECITE{Evolution}{% vanDiepen:1986:PDT% }. \NAMECITE{exception}{% Cocco:1982:MEH,% Szczepanska:1991:HLV% }. \NAMECITE{Exceptions}{% PeytonJones:1999:SIE,% Jones:1999:SIE% }. \NAMECITE{exchange}{% Hoare:2011:LEL% }. \NAMECITE{exclusion}{% Page:1989:SME% }. \NAMECITE{executable}{% Hoare:1984:PEP% }. \NAMECITE{exercise}{% Dijkstra:1989:ETH,% Hoare:1988:PCC% }. \NAMECITE{Experiment}{% Dijkstra:20xx:ERC% }. \NAMECITE{Experiments}{% Hoare:2008:VST,% Meyer:2008:VST% }. \NAMECITE{Exploring}{% Moller:2015:EIM% }. \NAMECITE{expressed}{% Sridhar:1985:JEC% }. \NAMECITE{expressions}{% Hoare:1964:CE% }. \NAMECITE{expressive}{% Hoofman:1991:WEM% }. \NAMECITE{Expressiveness}{% Bergstra:1982:ECH,% Olderog:1983:NER,% RodriguezArtalejo:1985:SQA% }. \NAMECITE{Extended}{% Hooman:1992:CVR% }. \NAMECITE{Extending}{% Hoare:2004:EHDa,% Hoare:2004:EHDb,% Hooman:1994:EHL% }. \NAMECITE{extensible}{% Chlipala:2013:BSP% }. \NAMECITE{Extension}{% Baeten:1990:CTC% }. \NAMECITE{F}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{fail}{% Bergstra:1982:SNS% }. \NAMECITE{Fast}{% Macnaghten:1977:FFT% }. \NAMECITE{Fault}{% Joseph:1987:PRF% }. \NAMECITE{Favorite}{% Kernighan:1984:WPM,% Kernighan:1981:WPM% }. \NAMECITE{{FBCS}}{% Black:2012:PSD% }. \NAMECITE{February}{% Hoare:1971:CSI,% Hoare:2004:RMN% }. \NAMECITE{{Fellow}}{% Dijkstra:1982:PTP% }. \NAMECITE{Fifteen}{% Mller:2021:FFY% }. \NAMECITE{fifteenth}{% ACM:1983:PFA% }. \NAMECITE{Fifty}{% Apt:2019:FYH% }. \NAMECITE{file}{% Chajed:2017:CFS% }. \NAMECITE{final}{% Bowen:1996:PIP,% Woodger:1969:MRA% }. \NAMECITE{{FIND}}{% Hoare:1971:PPF,% Fouz:2012:SAQ,% Hoare:1961:AF,% Prodinger:1995:MQH,% Kirschenhofer:1998:CHF% }. \NAMECITE{Finding}{% Brown:1976:RAA,% Floyd:1975:AAA,% Jones:2021:FEA% }. \NAMECITE{Fine}{% Dijkstra:1982:MSMa,% Hoare:2010:FGCa,% Hoare:2010:FGCb,% Dijkstra:1977:MSM,% Hoare:2008:VFG% }. \NAMECITE{Fine-Grain}{% Hoare:2010:FGCa,% Hoare:2010:FGCb,% Hoare:2008:VFG% }. \NAMECITE{Fine-Grained}{% Dijkstra:1982:MSMa,% Dijkstra:1977:MSM% }. \NAMECITE{First}{% Meyer:2008:VST,% Mller:2021:FFY,% Abdallah:2005:CSP,% Ashenhurst:1987:ATA% }. \NAMECITE{Fixed}{% Hoare:1990:FPI% }. \NAMECITE{Fixpoints}{% Guttmann:2019:CFC% }. \NAMECITE{flitting}{% Hoare:2004:VIF% }. \NAMECITE{Florida}{% Rishe:1990:PIC% }. \NAMECITE{flow}{% Bruni:2005:CTA,% Hoare:2011:UMD% }. \NAMECITE{{Floyd}}{% Arthan:2009:GFS,% Bloom:1991:FHL,% Chisholm:1989:ARP,% Pratt:1976:SCF,% Ying:2011:FHL% }. \NAMECITE{{Floyd-Hoare}}{% Arthan:2009:GFS% }. \NAMECITE{Follow}{% Hoare:2000:HAF% }. \NAMECITE{forecast}{% Hoare:1983:TF% }. \NAMECITE{Foreword}{% Hoare:1976:F,% Hoare:1994:F% }. \NAMECITE{Form}{% Hoare:1993:NFA% }. \NAMECITE{Formal}{% Barthe:2009:FCC,% Beckert:2006:ISF,% Hoare:1974:CCF,% Hoare:1987:OSF,% Hoare:1989:FMC,% Liu:2013:TPF,% Owe:2004:OOF,% Bjorner:1990:VVZ,% Fokkinga:1987:CPS% }. \NAMECITE{formula}{% Dijkstra:1999:FWT% }. \NAMECITE{Forty}{% Hoare:2022:FYE% }. \NAMECITE{Foundations}{% Hoare:2009:FCK,% IEEE:1976:ASF,% ODonnell:1982:CFH,% Hoare:1993:PPT,% Hoare:2011:CKA% }. \NAMECITE{{Fourier}}{% Macnaghten:1977:FFT% }. \NAMECITE{Fractional}{% Hoare:2004:FSP% }. \NAMECITE{Frame}{% Thielecke:2006:FRA% }. \NAMECITE{framework}{% Arthan:2009:GFS% }. \NAMECITE{Framing}{% Banerjee:2022:RPL% }. \NAMECITE{France}{% Wolff:2013:UTP% }. \NAMECITE{Francisco}{% Abadi:2005:CCT% }. \NAMECITE{Free}{% Macnaghten:1977:FFT,% Fournet:2004:SFC% }. \NAMECITE{FREng}{% Black:2012:PSD,% Hoare:2004:RMN% }. \NAMECITE{FRG}{% Bjorner:1990:VVZ% }. \NAMECITE{FRS}{% Black:2012:PSD% }. \NAMECITE{Function}{% Knijnenburg:1992:CIP% }. \NAMECITE{Functions}{% Clint:1972:PPJ,% Hoare:1972:OSTb,% Hoare:1990:FPI,% Ashcroft:1976:RPP% }. \NAMECITE{Gap}{% Hoare:1994:HSCa,% Hoare:1994:HSCb% }. \NAMECITE{garbage}{% Hoare:1974:OSS% }. \NAMECITE{GC6}{% Hoare:2004:EHDa% }. \NAMECITE{General}{% Enslow:1975:ILRb,% Arthan:2009:GFS,% Csirmaz:1981:PPV,% Hoare:1973:GCL% }. \NAMECITE{generalization}{% Stirling:1988:GOG% }. \NAMECITE{generalized}{% Nguyen:1986:GOMa% }. \NAMECITE{generative}{% Chlipala:2013:BSP% }. \NAMECITE{generator}{% Homeier:1995:MVV% }. \NAMECITE{Generic}{% Hoare:2013:GML% }. \NAMECITE{genetically}{% Bernot:2019:GMH% }. \NAMECITE{Geometry}{% Hoare:2019:CST,% Hoare:2019:CSTa% }. \NAMECITE{Georgia}{% Ryder:1999:PAS% }. \NAMECITE{Germany}{% Broy:1996:DPD,% Haddad:2012:ATP,% Hofner:2014:RAM% }. \NAMECITE{get}{% Hoare:1996:HDS% }. \NAMECITE{global}{% Olderog:1984:CPP% }. \NAMECITE{Good}{% Clarke:1979:PLC% }. \NAMECITE{{GOTO}}{% Lifschitz:1984:VPG% }. \NAMECITE{{GPU}}{% Kojima:2017:HLG% }. \NAMECITE{grail}{% Hoare:2003:KTK% }. \NAMECITE{Grain}{% Hoare:2010:FGCa,% Hoare:2008:VFG,% Hoare:2010:FGCb% }. \NAMECITE{Grained}{% Dijkstra:1982:MSMa,% Dijkstra:1977:MSM% }. \NAMECITE{Grand}{% Hoare:2003:VCGa,% Hoare:2004:GCC,% Hoare:2005:GCC,% Hoare:2008:VST,% Hoare:2003:VCGb,% Hoare:2005:VCG,% Woodcock:2021:VGC% }. \NAMECITE{grape}{% Hoare:2004:VIF% }. \NAMECITE{Graph}{% Poskitt:2012:HSV% }. \NAMECITE{Graphical}{% Wehrman:2009:GMS,% Zhan:2019:UGC% }. \NAMECITE{graphically}{% Page:1989:SME% }. \NAMECITE{graphs}{% Hoare:1979:CGW% }. \NAMECITE{gratitude}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{{Gries}}{% Stirling:1988:GOG% }. \NAMECITE{Guarantee}{% Hayes:2019:DAR% }. \NAMECITE{guards}{% Groote:1994:PAG% }. \NAMECITE{Guest}{% Hoare:1972:GEQ,% Hoare:1994:GE% }. \NAMECITE{guide}{% Hoare:1970:BRC% }. \NAMECITE{H}{% Brockhaus:1973:BRC% }. \NAMECITE{Hall}{% Anonymous:1987:BRC,% Horning:1989:BRE% }. \NAMECITE{Hamburg}{% Haddad:2012:ATP% }. \NAMECITE{hand}{% Hoare:2010:TPH% }. \NAMECITE{handling}{% Cocco:1982:MEH,% Hoare:1965:RH,% Hoare:1968:RH,% Szczepanska:1991:HLV% }. \NAMECITE{Hard}{% Hoare:2000:HAF% }. \NAMECITE{hardback}{% Horning:1989:BRE% }. \NAMECITE{Hardware}{% Hoare:1994:HSCa,% Hoare:1994:HSCb,% Gordon:1992:MRH% }. \NAMECITE{healthiness}{% He:2000:UTH% }. \NAMECITE{Hedges}{% Struth:2021:THA% }. \NAMECITE{held}{% Bauer:1976:LHI,% Broy:1996:DPD,% Ershov:1974:IST,% Gordon:1992:MRH% }. \NAMECITE{Help}{% Hoare:1993:MPM% }. \NAMECITE{Hemel}{% Horning:1989:BRE% }. \NAMECITE{Hempstead}{% Horning:1989:BRE% }. \NAMECITE{Hierarchical}{% Dahl:1972:HPS,% Dijkstra:1971:HOS% }. \NAMECITE{hierarchies}{% Bauer:1976:LHI% }. \NAMECITE{High}{% Hoare:1973:HLP,% Hoare:1976:HCP% }. \NAMECITE{Higher}{% Damm:1983:SRH,% Naumann:1995:PTH,% Shaner:2007:MVH,% Turon:2013:URH% }. \NAMECITE{higher-order}{% Naumann:1995:PTH,% Shaner:2007:MVH,% Turon:2013:URH% }. \NAMECITE{highly}{% Vafeiadis:2006:PCH% }. \NAMECITE{highly-concurrent}{% Vafeiadis:2006:PCH% }. \NAMECITE{Hints}{% Hoare:1973:HPLa,% Hoare:1973:HPLb,% Hoare:1973:HPLc,% Hoare:1974:HPL,% Hoare:1975:HDP,% Hoare:1976:HDP% }. \NAMECITE{Historic}{% Broy:2001:PTC,% Jones:2011:DHC% }. \NAMECITE{histories}{% Borgstrom:2011:RSH% }. \NAMECITE{Hoare}{% Anonymous:1987:BRC,% Barron:1975:BRS,% Barth:1974:BRJ,% Black:2012:PSD,% Brockhaus:1973:BRC,% Horning:1989:BRE,% Pritchard:1979:CPJ,% Ribeiro:2019:UTP,% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Anonymous:20xx:THE,% Apt:1981:TYH,% Apt:2019:FYH,% Apt:2021:ASI,% Arthan:2009:GFS,% Arthan:2013:HLL,% Ashcroft:1976:RPP,% Baer:1965:RPP,% Barthe:2012:PRH,% Bergstra:1982:ECH,% Bergstra:1982:SNS,% Bergstra:1982:TTA,% Bergstra:1983:HLP,% Bergstra:1984:ASP,% Bergstra:1984:HLP,% Bergstra:1984:PPI,% Bernot:2019:GMH,% Bloom:1991:FHL,% Borgstrom:2011:RSH,% Chajed:2017:CFS,% Cherniavsky:1979:CCH,% Chisholm:1989:ARP,% Chlipala:2013:BSP,% Clarke:1979:PLC,% Clarke:1983:EAH,% Coenen:1995:HLV,% Cohen:2000:NCP,% Dale:1994:CST,% Damm:1983:SRH,% Dasgupta:1984:UHL,% Davies:2000:MPC,% Daylight:2012:THM,% DeBoer:1997:HSC,% Delbianco:2013:HSR,% Dijkstra:1970:LPC,% Dijkstra:1974:LCR,% Dijkstra:1975:VTO,% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa,% Dijkstra:1982:PTP,% Dijkstra:1982:VTO,% Dijkstra:1989:ETH,% Dijkstra:1999:FWT,% Dijkstra:20xx:ERC,% Engelhardt:1996:SSS,% Feng:2021:QHL,% Flannery:1990:HSP,% Fouz:2012:SAQ,% Frana:2002:ICA,% Gardner:2008:LHR,% Greif:1981:SSW,% Groote:1994:PAG,% Grubel:1996:ADT,% Grubel:1998:HSA,% Hartog:2002:VPP,% Hoare:1980:HP,% Hoare:1982:VTO,% Hoofman:1991:WEM,% Hooman:1992:CVR,% Hooman:1994:EHL,% Hortala-Gonzalez:1989:HLN,% Huisman:2000:JPV,% Jacobs:2015:DHM,% Jones:2010:RWC,% Jones:2021:LTH,% Jones:2021:TPL,% Kirkerud:1982:CHC,% Kirschenhofer:1998:CHF,% Kleymann:1999:HLA,% Knijnenburg:1992:CIP,% Kojima:2017:HLG,% Kozen:2000:HLK,% Lamport:1980:HLC,% Lamport:1984:HLC,% Lloyd:1974:BRS,% Mamouras:2016:HLD,% Mancini:1988:HLD,% Nanevski:2006:PSH,% Nanevski:2008:HTT,% Neuhold:1977:UHM,% Nielson:1987:HLP,% Nipkow:2002:HLR,% ODonnell:1982:CFH,% Olderog:1981:SCH,% Olderog:1983:CHL,% Poskitt:2012:HSV% }. \NAMECITE{{Hoare}}{% Pratt:1976:SCF,% Prodinger:1995:MQH,% Reus:2001:HCV,% RodriguezArtalejo:1985:SQA,% Roscoe:1994:CME,% Saabas:2007:CNS,% Sergey:2016:HSS,% Shustek:2009:IIC,% Sokolowski:1987:SHL,% Sousa:2016:CHL,% Stirling:1988:GOG,% Sun:1996:TRH,% Szczepanska:1991:HLV,% Takaoka:1987:DRH,% Turon:2013:URH,% Wand:1976:NIR,% Wand:1978:NIR,% Woodcock:2021:HHU,% Xu:2016:CHL,% Ying:2011:FHL,% deBoer:2002:HLD,% deBoer:2021:CCR,% denHartog:2008:TMC,% vonHenke:1985:RHS,% vonOheimb:2001:HLJ,% vonOheimb:2002:HLN% }. \NAMECITE{{Hoare}-calculi}{% Kirkerud:1982:CHC% }. \NAMECITE{{Hoare}-like}{% Bergstra:1982:SNS,% Nielson:1987:HLP,% Olderog:1981:SCH,% Szczepanska:1991:HLV% }. \NAMECITE{{Hoare}-Logic}{% Damm:1983:SRH% }. \NAMECITE{{Hoare}-Style}{% Poskitt:2012:HSV,% DeBoer:1997:HSC,% Delbianco:2013:HSR,% Sergey:2016:HSS,% Turon:2013:URH% }. \NAMECITE{Hoares}{% Apt:1984:TYH% }. \NAMECITE{Hoc}{% Wu:2019:USC% }. \NAMECITE{{HOL}}{% vonOheimb:2001:HLJ% }. \NAMECITE{holy}{% Hoare:2003:KTK% }. \NAMECITE{honour}{% Davies:2000:MPC,% Roscoe:1994:CME% }. \NAMECITE{horizons}{% Hoare:2004:EHDa,% Hoare:2004:EHDb% }. \NAMECITE{horizontal}{% Dasgupta:1984:UHL% }. \NAMECITE{Houston}{% IEEE:1976:ASF% }. \NAMECITE{Hrsg}{% Brockhaus:1973:BRC% }. \NAMECITE{Hybrid}{% Foster:2019:HRI% }. \NAMECITE{ICCSW'13}{% Jones:2013:ICC% }. \NAMECITE{idea}{% Fetzer:1988:PVV% }. \NAMECITE{Ideal}{% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Hoare:2007:IPC,% Hoare:2006:IVS% }. \NAMECITE{If}{% Lewis:1997:BCI% }. \NAMECITE{{IFIP}}{% Meyer:2008:VST% }. \NAMECITE{Ignore}{% Welch:1997:LEI% }. \NAMECITE{{II}}{% Apt:1984:TYH,% Bowen:1996:PIP,% Enslow:1975:ILRb,% Hoare:1986:WPb% }. \NAMECITE{III}{% Hoare:2001:ETS,% Enslow:1975:ILRc% }. \NAMECITE{Impact}{% Apt:2021:ASI% }. \NAMECITE{imperative}{% Nanevski:2008:YDT% }. \NAMECITE{Imperial}{% Jones:2013:ICC% }. \NAMECITE{Implementation}{% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Ryder:1999:PAS% }. \NAMECITE{implementations}{% Hoare:1982:SPI% }. \NAMECITE{Impossible}{% Clarke:1979:PLC% }. \NAMECITE{Imprecise}{% PeytonJones:1999:SIE,% Jones:1999:SIE% }. \NAMECITE{Inadequacy}{% Blass:2001:ICL% }. \NAMECITE{inaugural}{% Hoare:1971:CSI,% Hoare:1986:MPI% }. \NAMECITE{inclusion}{% Bergstra:1984:PPI% }. \NAMECITE{Incompleteness}{% Wand:1978:NIR,% Wand:1976:NIR% }. \NAMECITE{Incomputability}{% Hoare:1972:I% }. \NAMECITE{increasing}{% Hoare:1990:FPI% }. \NAMECITE{independent}{% vanAmmers:1998:PCC% }. \NAMECITE{Index}{% Jones:2021:ABI% }. \NAMECITE{indirect}{% Hoare:1965:NIA% }. \NAMECITE{inductive}{% Chisholm:1989:ARP% }. \NAMECITE{Industrial}{% Bottaci:2010:TAI% }. \NAMECITE{Inform}{% Pettersson:1991:LEC,% Santini:2005:WSI,% VanGasteren:1990:CPD% }. \NAMECITE{{Infotech}}{% Bates:1976:SPI% }. \NAMECITE{initiative}{% Hoare:2009:VSI,% Hoare:2021:VSI% }. \NAMECITE{{Inmos}}{% May:2021:COI% }. \NAMECITE{Inner}{% Butterfield:2019:IOA% }. \NAMECITE{input}{% Hoare:1963:EAI% }. \NAMECITE{input/output}{% Hoare:1963:EAI% }. \NAMECITE{inputs}{% Xu:2016:CHL% }. \NAMECITE{Insecurities}{% Welsh:1977:AIP% }. \NAMECITE{Institute}{% Broy:1996:DPD% }. \NAMECITE{Intelligent}{% Beckert:2006:ISF% }. \NAMECITE{Intensive}{% Broy:2005:ETS% }. \NAMECITE{interesting}{% Hoare:2000:SLI% }. \NAMECITE{interface}{% Moller:2015:EIM% }. \NAMECITE{interfaces}{% Bauer:1976:LHI% }. \NAMECITE{International}{% Abadi:2005:CCT,% Anonymous:1987:BRC,% Berghammer:2009:RKA,% Bjorner:1990:VVZ,% Bottaci:2010:TAI,% Gibbons:2012:MPC,% Haddad:2012:ATP,% Hofner:2014:RAM,% Horning:1989:BRE,% IEEE:2002:AIC,% Kapur:1992:ADC,% Ribeiro:2019:UTP,% Rishe:1990:PIC,% Wolff:2013:UTP,% Bauer:1976:LHI,% Ershov:1974:IST% }. \NAMECITE{Interpretation}{% Knijnenburg:1992:CIP% }. \NAMECITE{Interpreting}{% Milner:1990:IOC% }. \NAMECITE{Interview}{% Frana:2002:ICA,% Jones:2021:AI,% Shustek:2009:IIC,% Black:2012:PSD% }. \NAMECITE{Introduction}{% Hoare:1977:I,% Shankar:1993:IAR% }. \NAMECITE{introductory}{% Hoare:1976:SPI% }. \NAMECITE{invariance}{% Pettersson:1991:LEC% }. \NAMECITE{invariant}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{invariants}{% Blass:2001:ICL% }. \NAMECITE{invited}{% Abdallah:2005:CSP,% Hoare:2000:LC,% Hoare:2006:IVS% }. \NAMECITE{Ireland}{% Hoare:1972:OST% }. \NAMECITE{{Iris}}{% Hoare:2004:VIF% }. \NAMECITE{Isabelle}{% Foster:2019:HRI,% vonOheimb:2001:HLJ% }. \NAMECITE{{Isabelle/HOL}}{% vonOheimb:2001:HLJ% }. \NAMECITE{Isabelle/{UTP}}{% Foster:2019:HRI% }. \NAMECITE{ISBN}{% Horning:1989:BRE% }. \NAMECITE{Isn't}{% Olsen:1997:LWJ% }. \NAMECITE{Issue}{% Hoare:2021:PSI,% Hoare:2009:PSI% }. \NAMECITE{Item}{% Dijkstra:1970:NIM% }. \NAMECITE{Iteration}{% Bloom:1991:FHL% }. \NAMECITE{J}{% Barron:1975:BRS,% Barth:1974:BRJ,% Lloyd:1974:BRS,% Pritchard:1979:CPJ% }. \NAMECITE{{J.}}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{{Jackson}}{% Hoare:2010:MJD% }. \NAMECITE{{Java}}{% Huisman:2000:JPV,% Lewis:1997:BCI,% Olsen:1997:LWJ,% Reus:2001:HCV,% Struble:1997:LDJ,% vonOheimb:2001:HLJ% }. \NAMECITE{{Jifeng}}{% Liu:2013:TPF% }. \NAMECITE{{Johan}}{% Owe:2004:OOF% }. \NAMECITE{Jones}{% Horning:1989:BRE% }. \NAMECITE{{Journal}}{% Hoare:2007:IPC% }. \NAMECITE{{JSD}}{% Sridhar:1985:JEC% }. \NAMECITE{July}{% Abdallah:2005:CSP,% Bauer:1976:LHI,% Broy:1996:DPD,% Hoare:2001:ETS,% IEEE:1988:ASL,% Dijkstra:1974:LCR% }. \NAMECITE{Jumps}{% Ashcroft:1976:RPP,% Clint:1972:PPJ% }. \NAMECITE{June}{% Broy:2001:PTC,% Gibbons:2012:MPC,% Haddad:2012:ATP,% Kapur:1992:ADC,% Lenzerini:2008:PTS% }. \NAMECITE{{{{KDF9}}}}{% Hoare:1964:BRA% }. \NAMECITE{Kernels}{% Kojima:2017:HLG% }. \NAMECITE{Key}{% Hoare:1997:UTC% }. \NAMECITE{Keynote}{% Hoare:1990:LMM,% Hoare:1990:RAPb,% Hoare:1991:TCC,% Hoare:1978:SEK% }. \NAMECITE{Kiel}{% Bjorner:1990:VVZ% }. \NAMECITE{King}{% Hoare:2003:KTK% }. \NAMECITE{Kingdom}{% Horning:1989:BRE,% Jones:2013:ICC% }. \NAMECITE{Kleene}{% Berghammer:2009:RKA,% Berghammer:2009:RKA,% Hoare:2009:CKA,% Hoare:2009:FCK,% Hoare:2011:CKA,% Hoare:2014:DCK,% Hoare:2016:DCK,% Kozen:2000:HLK% }. \NAMECITE{knights}{% Hoare:2003:KTK% }. \NAMECITE{{Knuth}}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{Language}{% Cherniavsky:1979:CCH,% Clarke:1979:PLC,% Damm:1983:SRH,% Enslow:1975:ILRb,% Hoare:1972:ADP,% Hoare:1973:ADP,% Hoare:1973:HPLa,% Hoare:1973:HPLb,% Hoare:1973:HPLc,% Hoare:1974:ACA,% Hoare:2005:TSO,% Kernighan:1984:WPM,% Ryder:1999:PAS,% Hoare:1972:PBP,% Hoare:1974:ADP,% Hoare:1974:HPL,% Hoare:1975:HDP,% Hoare:1976:HDP,% Hoare:1989:VPL,% Hoare:1990:AAV,% Kernighan:1981:WPM,% Stirling:1988:GOG,% Szczepanska:1991:HLV,% Bauer:1976:LHI,% Hoare:1996:PPA% }. \NAMECITE{Languages}{% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Feuer:1984:CAP,% Hoare:1974:CCF,% Hoare:1985:MLP,% Bergstra:1984:HLP,% He:1990:CSP,% Hoare:1968:LL,% Hoare:1970:BRC,% Hoare:1973:HLP,% Hoare:1976:HCP,% Hoare:1990:CSP,% Saabas:2007:CNS,% Hoare:1970:BRC% }. \NAMECITE{{LASER}}{% Muller:2010:ALS% }. \NAMECITE{{Lauer}}{% Greif:1981:SSW% }. \NAMECITE{law}{% Hoare:1973:GCL,% Hoare:2011:LEL% }. \NAMECITE{Laws}{% Hoare:1987:CLP,% Hoare:1987:LP,% Hoare:1992:LP,% Hoare:1993:MPM,% Hoare:2012:LPU,% Hoare:2013:GML,% Hoare:2013:LPC,% Hoare:2014:LCP,% Roscoe:1986:LOP,% Hoare:2014:LPU,% Roscoe:1988:LOP% }. \NAMECITE{{LCF}}{% Sokolowski:1987:SHL% }. \NAMECITE{Learning}{% Hoare:2002:LLU% }. \NAMECITE{lecture}{% Hoare:1971:CSI,% Hoare:1986:MPI,% Hoare:2007:IPC,% Hoare:2021:ATA% }. \NAMECITE{lectures}{% Muller:2010:ALS,% Ashenhurst:1987:ATA% }. \NAMECITE{Legacy}{% Apt:2022:EWD,% Hoare:2000:LC,% Hoare:2001:L% }. \NAMECITE{Let}{% Hoare:1990:LMM% }. \NAMECITE{Lett}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{Letter}{% Dijkstra:1970:LPC,% Hoare:1966:LWM,% Hoare:1968:LVW,% Hoare:1982:VTO,% Pettersson:1991:LEC,% Dijkstra:1974:LCR,% Dijkstra:1975:VTO,% Dijkstra:1982:VTO% }. \NAMECITE{Letters}{% Gozum:1997:LWC,% McReynolds:1997:LBS,% Olsen:1997:LWJ,% Struble:1997:LDJ,% Welch:1997:LEI% }. \NAMECITE{level}{% Hoare:1968:DST,% Hoare:1973:HLP,% Hoare:1990:AAV,% Saabas:2007:CNS% }. \NAMECITE{Life}{% Apt:2022:EWD,% Jones:2021:TPL,% Hoare:2000:SLI% }. \NAMECITE{Like}{% Hartog:2002:VPP,% Bergstra:1982:SNS,% Hoare:2004:YWT,% LeGuyadec:1996:SLP,% Nielson:1987:HLP,% Olderog:1981:SCH,% Olderog:1984:CPP,% Szczepanska:1991:HLV,% Olderog:1983:CHL% }. \NAMECITE{Limitations}{% Hoare:1968:LL% }. \NAMECITE{linear}{% Arthan:2013:HLL% }. \NAMECITE{linearisable}{% Vafeiadis:2006:PCH% }. \NAMECITE{linearizable}{% Sergey:2016:HSS% }. \NAMECITE{Linking}{% He:1997:LTP,% He:1999:LTP,% He:2005:LTC% }. \NAMECITE{List}{% Jones:2021:LTH,% vanDiepen:1986:PDT% }. \NAMECITE{List-Copying}{% vanDiepen:1986:PDT% }. \NAMECITE{Local}{% Gardner:2008:LHR% }. \NAMECITE{locality}{% Hoare:2011:LEL% }. \NAMECITE{Logic}{% Apt:1981:TYH,% Apt:2021:ASI,% Banerjee:2022:RPL,% Bergstra:1982:TTA,% Bergstra:1984:ASP,% Bloom:1991:FHL,% Broy:2003:MAL,% Damm:1983:SRH,% Feng:2021:QHL,% Hartog:2002:VPP,% Hoare:1985:MLP,% Hoare:2008:SLS,% Hoare:2019:CST,% Huisman:2000:JPV,% IEEE:1988:ASL,% Kleymann:1999:HLA,% Knijnenburg:1992:CIP,% Kojima:2017:HLG,% Lamport:1980:HLC,% Lamport:1984:HLC,% Mamouras:2016:HLD,% Sokolowski:1987:SHL,% deBoer:2021:CCR,% vonOheimb:2002:HLN,% Apt:1984:TYH,% Apt:2019:FYH,% Arthan:2013:HLL,% Becker:2010:LSM,% Bergstra:1982:ECH,% Bergstra:1982:SNS,% Bergstra:1983:HLP,% Bergstra:1984:HLP,% Bergstra:1984:PPI,% Bernot:2019:GMH,% Brotherston:2008:CPP,% Chajed:2017:CFS,% Chlipala:2013:BSP,% Coenen:1995:HLV,% Cohen:2000:NCP,% Dasgupta:1984:UHL,% Daylight:2012:THM,% Engelhardt:1996:SSS,% Groote:1994:PAG,% Hoare:1988:PCC,% Hoare:1996:LED,% Hoare:2001:UTL,% Hoare:2019:CSTa,% Hoofman:1991:WEM,% Hooman:1994:EHL,% Hortala-Gonzalez:1989:HLN,% Kozen:2000:HLK,% Mancini:1988:HLD,% Olderog:1983:CHL,% Pratt:1976:SCF,% RodriguezArtalejo:1985:SQA,% Saabas:2007:CNS,% Seres:1999:ALP,% Sousa:2016:CHL,% Stirling:1988:GOG,% Sun:1996:TRH,% Takaoka:1987:DRH,% Turon:2013:URH,% Wehrman:2009:GMS,% Xu:2016:CHL,% Ying:2011:FHL,% deBoer:2002:HLD,% denHartog:2008:TMC,% vonOheimb:2001:HLJ% }. \NAMECITE{Logics}{% Barthe:2012:PRH,% Clarke:1983:EAH,% Nipkow:2002:HLR,% ODonnell:1982:CFH,% Arthan:2009:GFS% }. \NAMECITE{London}{% Abdallah:2005:CSP,% Anonymous:1976:SSE,% Anonymous:1987:BRC,% Barron:1975:BRS,% Jones:2013:ICC% }. \NAMECITE{Long}{% Butler:2005:TSL% }. \NAMECITE{Long-Running}{% Butler:2005:TSL% }. \NAMECITE{loop}{% Blass:2001:ICL% }. \NAMECITE{love}{% Hoare:2002:LLU% }. \NAMECITE{low}{% Saabas:2007:CNS% }. \NAMECITE{low-level}{% Saabas:2007:CNS% }. \NAMECITE{M}{% Hoare:1970:BRC% }. \NAMECITE{{M.}}{% Ashcroft:1976:RPP% }. \NAMECITE{M1}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{Machine}{% Hoare:1961:MSS,% Boyer:1992:ACP,% Hoare:2004:YWT% }. \NAMECITE{Machines}{% Bazilevskii:1963:TMM,% Baer:1965:RPP% }. \NAMECITE{Madrid}{% Gibbons:2012:MPC% }. \NAMECITE{mail}{% Hoare:1986:ASP,% Hoare:1987:DPM,% Hoare:1991:DPM% }. \NAMECITE{make}{% Hoare:1990:LMM% }. \NAMECITE{Making}{% Dijkstra:1982:MSMa,% Dijkstra:1977:MSM% }. \NAMECITE{management}{% Hoare:1972:SSMa,% Hoare:1972:SSMb% }. \NAMECITE{mandatory}{% Shaner:2007:MVH% }. \NAMECITE{Manifesto}{% Hoare:2021:VSI,% Hoare:2009:VSI% }. \NAMECITE{manipulation}{% Hoare:1968:SM% }. \NAMECITE{manual}{% Spivey:1989:ZNR% }. \NAMECITE{March}{% Hoare:2004:RMN,% Rishe:1990:PIC% }. \NAMECITE{Marienstatt}{% Hofner:2014:RAM% }. \NAMECITE{{Markov}}{% Grubel:1998:HSA% }. \NAMECITE{Marktoberdorf}{% Bauer:1976:LHI,% Broy:1996:DPD,% Hoare:2001:ETS% }. \NAMECITE{Massachusetts}{% ACM:1983:PFA% }. \NAMECITE{Mathematical}{% Baer:1965:RPP,% Bazilevskii:1963:TMM,% Hoare:1985:MLP,% Hoare:1993:MPM,% Hoare:1996:MMC,% Daylight:2012:THM,% Hoare:1981:TMB% }. \NAMECITE{Mathematics}{% Gibbons:2012:MPC,% Hoare:1986:MP,% Hoare:1993:MPM,% Hoare:1985:MP,% Hoare:1986:MPI% }. \NAMECITE{Maths}{% Hoare:1986:MAS% }. \NAMECITE{Matrix}{% Johnston:1975:MRE% }. \NAMECITE{May}{% Hofner:2014:RAM,% Ryder:1999:PAS,% VanGasteren:1990:CPD% }. \NAMECITE{means}{% Fokkinga:1987:CPS% }. \NAMECITE{mechanically}{% Homeier:1995:MVV% }. \NAMECITE{mechanism}{% Cocco:1982:MEH,% Szczepanska:1991:HLV% }. \NAMECITE{Mechanized}{% Gordon:1992:MRH,% denHartog:2008:TMC% }. \NAMECITE{Meeting}{% Hoare:1999:TPT,% Gordon:1992:MRH,% Hoare:1993:WSE% }. \NAMECITE{members}{% Hoare:1966:LWM% }. \NAMECITE{memoriam}{% Boyer:2002:MEW% }. \NAMECITE{Memory}{% Manna:2010:TVE,% Owe:2004:OOF% }. \NAMECITE{men}{% Hoare:1973:TMR% }. \NAMECITE{menu}{% Enikeev:1987:MTC% }. \NAMECITE{menu-dialog}{% Enikeev:1987:MTC% }. \NAMECITE{Message}{% Hoare:2012:MT,% Hoare:2012:MTR,% Stoller:1995:VPU% }. \NAMECITE{message-passing}{% Stoller:1995:VPU% }. \NAMECITE{metaprogramming}{% Chlipala:2013:BSP% }. \NAMECITE{Method}{% Hoare:1961:MSS,% Johnston:1975:MRE,% Neuhold:1977:UHM,% Pritchard:1979:CPJ% }. \NAMECITE{Methods}{% Beckert:2006:ISF,% Berghammer:2009:RKA,% Hoare:1987:OSF,% Hofner:2014:RAM,% Liu:2013:TPF,% Owe:2004:OOF,% Welch:1997:LEI,% vonOheimb:2002:HLN,% Bjorner:1990:VVZ,% Chisholm:1989:ARP,% Hoare:1989:FMC,% Shaner:2007:MVH% }. \NAMECITE{Miami}{% Rishe:1990:PIC% }. \NAMECITE{Michael}{% Hoare:2004:RMN,% Hoare:2010:MJD% }. \NAMECITE{Microcomputer}{% Ekanadham:1981:MN% }. \NAMECITE{microprocessor}{% Boyer:1992:ACP,% Boyer:1996:APO% }. \NAMECITE{microprograms}{% Dasgupta:1984:UHL% }. \NAMECITE{Microsoft}{% Davies:2000:MPC% }. \NAMECITE{Middle}{% Hoare:1999:TPT% }. \NAMECITE{{Millennial}}{% Davies:2000:MPC% }. \NAMECITE{{Mind}}{% Roscoe:1994:CME% }. \NAMECITE{Minority}{% Dijkstra:1970:NIM,% Woodger:1969:MRA% }. \NAMECITE{Mobile}{% Wu:2019:USC% }. \NAMECITE{modality}{% Winskel:1985:PM% }. \NAMECITE{Model}{% Enikeev:1987:MTC,% Hoare:1999:TMPb,% Gritzner:1996:RAM,% Hehner:1983:MCM,% Hoare:1980:MCSa,% Hoare:1980:MCSb,% Hoare:1981:MCS,% Hoare:1990:MSS,% Hoare:1999:TMPa,% Moller:2015:EIM,% Nguyen:1986:GOMa,% Shaner:2007:MVH,% Xu:2016:CHL,% Zhou:1992:MSS% }. \NAMECITE{modelling}{% Zhan:2019:UGC% }. \NAMECITE{Models}{% Broy:2003:MAL,% Hoare:1993:AMb,% Hoare:2012:NMC,% Hoare:2013:GML,% Reus:2001:HCV,% Hoare:1990:LMM,% Hoare:1992:AM,% Hoare:1993:AMa,% Hoare:1995:AM,% Hoare:1996:AM,% Hoare:1996:MMC,% Hoare:2011:UMD,% Hoofman:1991:WEM,% Wehrman:2009:GMS% }. \NAMECITE{modern}{% Hoare:2002:AMS% }. \NAMECITE{modified}{% Bernot:2019:GMH% }. \NAMECITE{modifying}{% Becker:2010:LSM,% Cai:2007:CSM% }. \NAMECITE{Modular}{% Shaner:2007:MVH% }. \NAMECITE{Monadic}{% Mamouras:2016:HLD,% Jacobs:2015:DHM% }. \NAMECITE{monads}{% Jacobs:2015:DHM% }. \NAMECITE{Monitor}{% Welch:1997:LEI% }. \NAMECITE{Monitors}{% Hoare:1974:MOS,% Hoare:2002:MOS% }. \NAMECITE{{MOS}}{% Hoare:1988:PCC,% Hoare:1990:TDC,% Hoare:1991:TDCa,% Hoare:1991:TDCb% }. \NAMECITE{MPC}{% Gibbons:2012:MPC% }. \NAMECITE{MR}{% Pritchard:1979:CPJ% }. \NAMECITE{{Multiple}}{% Prodinger:1995:MQH% }. \NAMECITE{Multiprocessors}{% Elliott:1989:SAM% }. \NAMECITE{mutual}{% Page:1989:SME% }. \NAMECITE{My}{% Kernighan:1984:WPM,% Kernighan:1981:WPM% }. \NAMECITE{Name}{% Cipra:2000:BCE% }. \NAMECITE{{NanoJava}}{% vonOheimb:2002:HLN% }. \NAMECITE{{NATO}}{% Broy:1996:DPD,% Hoare:2001:ETS% }. \NAMECITE{natural}{% Bergstra:1982:SNS,% Saabas:2007:CNS% }. \NAMECITE{Needham}{% Hoare:2004:RMN,% Herbert:2004:CST% }. \NAMECITE{Net}{% Hoare:2012:NMC% }. \NAMECITE{Nets}{% Haddad:2012:ATP% }. \NAMECITE{network}{% Hoare:1985:SSN,% Morgan:1985:SSN% }. \NAMECITE{Networks}{% Ekanadham:1981:MN,% Wu:2019:USC,% deBoer:2002:HLD% }. \NAMECITE{{Neuhold}}{% Pritchard:1979:CPJ% }. \NAMECITE{Newnes}{% Hoare:1970:BRC% }. \NAMECITE{Newnes-Butterworths}{% Hoare:1970:BRC% }. \NAMECITE{News}{% Dijkstra:1970:NIM% }. \NAMECITE{No}{% Barron:1975:BRS,% Hoare:1987:CLP,% Pritchard:1979:CPJ% }. \NAMECITE{non}{% Hoare:1980:TND,% Sergey:2016:HSS% }. \NAMECITE{non-determinism}{% Hoare:1980:TND% }. \NAMECITE{non-linearizable}{% Sergey:2016:HSS% }. \NAMECITE{Nondeterminism}{% Apt:1984:TYH,% Nipkow:2002:HLR,% Francez:1978:SNC,% Francez:1979:SNC,% Kennaway:1980:TN% }. \NAMECITE{Nondeterministic}{% Mamouras:2016:HLD,% Hortala-Gonzalez:1989:HLN% }. \NAMECITE{nonstandard}{% Hortala-Gonzalez:1989:HLN% }. \NAMECITE{Normal}{% Hoare:1993:NFA% }. \NAMECITE{Northern}{% Hoare:1972:OST% }. \NAMECITE{notation}{% Spivey:1989:ZNR% }. \NAMECITE{Note}{% Hoare:1972:NS,% Cohen:2000:NCP,% Hoare:1965:NIA% }. \NAMECITE{Notes}{% Dijkstra:1972:NSP,% Hoare:1972:NDS,% Hoare:1983:NCS,% Hoare:1985:NCS,% Hoare:1986:NCS,% Hoare:1989:NAC% }. \NAMECITE{notion}{% Olderog:1983:NER% }. \NAMECITE{novelties}{% Hoare:1985:CNP% }. \NAMECITE{November}{% Berghammer:2009:RKA% }. \NAMECITE{Novosibirsk}{% Ershov:1974:IST% }. \NAMECITE{NY}{% Kapur:1992:ADC% }. \NAMECITE{nye}{% Khoar:1989:CVC% }. \NAMECITE{O}{% Barron:1975:BRS,% Lloyd:1974:BRS% }. \NAMECITE{{O.}}{% Barth:1974:BRJ% }. \NAMECITE{O.-J}{% Barron:1975:BRS,% Lloyd:1974:BRS% }. \NAMECITE{Object}{% Hoare:2012:NMC,% Owe:2004:OOF,% Boyer:1996:APO,% Nguyen:1986:GOMa% }. \NAMECITE{Object-Orientation}{% Owe:2004:OOF% }. \NAMECITE{objectives}{% Hoare:1972:OSTb% }. \NAMECITE{Objects}{% Hoare:1999:TMPb,% Hoare:1999:TMPa,% Sergey:2016:HSS,% Vafeiadis:2006:PCH% }. \NAMECITE{Obtain}{% Clarke:1979:PLC% }. \NAMECITE{occam}{% Hoare:1991:TOP,% May:2021:COI,% Roscoe:1986:LOP,% Roscoe:1988:LOP% }. \NAMECITE{Occasion}{% Jones:2011:DHC,% Liu:2013:TPF,% Abdallah:2005:CSP,% Dijkstra:1982:PTP,% Ribeiro:2019:UTP% }. \NAMECITE{{OCL}}{% Reus:2001:HCV% }. \NAMECITE{{OCL}-Constrained}{% Reus:2001:HCV% }. \NAMECITE{October}{% Gordon:1992:MRH,% Hoare:1986:MPI,% IEEE:1976:ASF,% Meyer:2008:VST,% Ribeiro:2019:UTP% }. \NAMECITE{Oh}{% Weiss:1988:BOP% }. \NAMECITE{Old}{% Hoare:1981:EOC,% Hoare:1987:EOC% }. \NAMECITE{{Ole}}{% Owe:2004:OOF% }. \NAMECITE{{Ole-Johan}}{% Owe:2004:OOF% }. \NAMECITE{one}{% Milner:1990:IOC% }. \NAMECITE{Online}{% Gray:2021:OR% }. \NAMECITE{Open}{% Hoare:1982:VTO,% Dijkstra:1975:VTO,% Dijkstra:1982:VTO% }. \NAMECITE{Operating}{% Brockhaus:1973:BRC,% Hoare:1972:OSTb,% Hoare:1974:MOS,% Hoare:1982:SOS,% Hoare:2002:MOS,% Hoare:1976:SOS,% Hoare:1972:OST% }. \NAMECITE{Operational}{% Aichernig:2019:TPA,% Hoare:1994:ACO,% vanStaden:2013:AUO,% He:1993:AOS,% Hoare:1997:ADO,% Hoare:2000:ADO,% Ridge:2009:VDS% }. \NAMECITE{optimisation}{% Jones:2001:PRR% }. \NAMECITE{Optimization}{% Hoare:1974:OSS% }. \NAMECITE{Orchestration}{% Hoare:2005:TSO% }. \NAMECITE{order}{% Makowsky:1989:WSO,% Martin:1991:PAO,% Naumann:1995:PTH,% Shaner:2007:MVH,% Turon:2013:URH% }. \NAMECITE{ordered}{% Stoller:1995:VPU% }. \NAMECITE{Ordering}{% Dijkstra:1971:HOS% }. \NAMECITE{Orientation}{% Owe:2004:OOF% }. \NAMECITE{Oriented}{% Olderog:1986:SOS,% Olderog:1983:SOS% }. \NAMECITE{Origin}{% BrinchHansen:2002:OCP% }. \NAMECITE{Original}{% Broy:2001:PTC% }. \NAMECITE{our}{% Feijen:1990:BOB% }. \NAMECITE{Outer}{% Butterfield:2019:IOA% }. \NAMECITE{output}{% Hoare:1963:EAI% }. \NAMECITE{Overview}{% Hoare:1987:OSF,% Kapur:1994:OTP% }. \NAMECITE{{Owicki}}{% Stirling:1988:GOG% }. \NAMECITE{Oxford}{% Davies:2000:MPC,% IEEE:2002:AIC,% Hoare:1986:MPI,% Sufrin:2021:TBO% }. \NAMECITE{Pacific}{% IEEE:2000:PSA% }. \NAMECITE{pages}{% Barron:1975:BRS,% Anonymous:1987:BRC% }. \NAMECITE{paging}{% Hoare:1973:SPS% }. \NAMECITE{Paper}{% Greif:1981:SSW,% Pritchard:1979:CPJ% }. \NAMECITE{Papers}{% Meyer:2008:VST,% Anonymous:1976:SSE,% Wolff:2013:UTP,% Abdallah:2005:CSP% }. \NAMECITE{parable}{% Hoare:1974:SDP% }. \NAMECITE{Parallel}{% Hoare:1972:TTP,% Hoare:1975:PPA,% Hoare:1976:PPA,% Hoare:1993:PPT,% Hoare:1997:UTPb,% Hoare:2002:TTP,% Hoare:1980:SPP,% LeGuyadec:1996:SLP,% Rishe:1990:PIC% }. \NAMECITE{parameters}{% Hoare:1971:PPA% }. \NAMECITE{{PARBASE}}{% Rishe:1990:PIC% }. \NAMECITE{{PARBASE-90}}{% Rishe:1990:PIC% }. \NAMECITE{Paris}{% Wolff:2013:UTP% }. \NAMECITE{PART}{% Bottaci:2010:TAI,% Hoare:1972:SSMa,% Hoare:1972:SSMb,% Anonymous:1976:SSE,% Apt:1981:TYH% }. \NAMECITE{Partial}{% Hoare:1981:PCC,% Hoare:1988:PCC,% Knijnenburg:1992:CIP,% Zhou:1981:PCC% }. \NAMECITE{{Partition}}{% Hoare:1961:AP% }. \NAMECITE{{PASCAL}}{% Hoare:1972:ADP,% Hoare:1974:ADP,% Olderog:1984:CPP,% Feuer:1984:CAP,% Hoare:1973:ADP,% Kernighan:1981:WPM,% Kernighan:1984:WPM,% Olderog:1983:CHL,% Welsh:1977:AIP,% Hoare:1974:ACA% }. \NAMECITE{{PASCAL}-like}{% Olderog:1984:CPP,% Olderog:1983:CHL% }. \NAMECITE{pass}{% Hoare:1966:SPC% }. \NAMECITE{passing}{% Stoller:1995:VPU% }. \NAMECITE{{Peano}}{% Bergstra:1983:HLP% }. \NAMECITE{peeled}{% Hoare:2004:VIF% }. \NAMECITE{Perrot}{% Brockhaus:1973:BRC% }. \NAMECITE{Personal}{% Dijkstra:1982:SWC,% Hoare:1991:TOP,% Hoare:2002:APP,% Hoare:2003:APP,% Hoare:1996:UTP% }. \NAMECITE{Perspective}{% Aichernig:2019:TPA,% Dijkstra:1982:SWC,% Hoare:2002:APP,% Hoare:2003:APP,% JaJa:2000:PQ% }. \NAMECITE{perspectives}{% Davies:2000:MPC% }. \NAMECITE{Peter}{% Hoare:1970:BRC% }. \NAMECITE{Petri}{% Haddad:2012:ATP% }. \NAMECITE{Physical}{% Zhan:2019:UGC% }. \NAMECITE{pictures}{% Dijkstra:1999:FWT% }. \NAMECITE{Pioneers}{% Broy:2001:PTC,% Broy:2002:SPC,% Weiss:1988:BOP,% Broy:2001:PTC% }. \NAMECITE{{PL}}{% Hoare:1966:P% }. \NAMECITE{{PL/I}}{% Hoare:1966:P% }. \NAMECITE{Playing}{% Jones:2001:PRR% }. \NAMECITE{PLDI}{% Ryder:1999:PAS% }. \NAMECITE{{Pnueli}}{% Manna:2010:TVE% }. \NAMECITE{PODS'08}{% Lenzerini:2008:PTS% }. \NAMECITE{Pointers}{% Hoare:1999:TMPb,% Hoare:1999:TMPa,% Ni:2006:CAP,% Thielecke:2006:FRA% }. \NAMECITE{points}{% Hoare:1990:FPI% }. \NAMECITE{policies}{% Becker:2010:LSM% }. \NAMECITE{Polymorphism}{% Nanevski:2006:PSH,% Nanevski:2008:HTT% }. \NAMECITE{Port}{% Silberschatz:1981:PDC% }. \NAMECITE{Porto}{% Ribeiro:2019:UTP% }. \NAMECITE{Portugal}{% Ribeiro:2019:UTP% }. \NAMECITE{posledovatel\cprime}{% Khoar:1989:CVC% }. \NAMECITE{possess}{% Bergstra:1982:SNS% }. \NAMECITE{possible}{% Tennent:1991:CPW% }. \NAMECITE{possible-world}{% Tennent:1991:CPW% }. \NAMECITE{power}{% Flannery:1990:HSP% }. \NAMECITE{powerdomains}{% Winskel:1985:PM% }. \NAMECITE{pp}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{Practical}{% Brookes:2021:CPP,% Shapiro:2006:PPC,% Hoare:1970:BRC,% Jones:2001:PRR% }. \NAMECITE{Practice}{% Bottaci:2010:TAI,% Hoare:2002:APS,% Hoare:2002:AMS% }. \NAMECITE{praise}{% Hoare:2012:PA% }. \NAMECITE{Pre}{% Martin:1991:PAO% }. \NAMECITE{Pre-adjunctions}{% Martin:1991:PAO% }. \NAMECITE{Predicate}{% Hoare:1978:SPP,% Naumann:1995:PTH,% Dijkstra:1982:PTP% }. \NAMECITE{predicates}{% Dijkstra:1982:PTP,% Hoare:1984:PEP,% Hoare:1984:PP,% Hoare:1985:PP,% Hoare:1993:PP% }. \NAMECITE{Preface}{% Hoare:1986:P,% Hoare:1996:PAB,% Hoare:1996:PPA,% Hoare:1996:PPC,% Hoare:1996:PQ,% Hoare:2009:PSI,% Hoare:2021:PSI,% Jones:2021:P,% Hoare:1996:PPA% }. \NAMECITE{Prentice}{% Anonymous:1987:BRC,% Horning:1989:BRE% }. \NAMECITE{Prentice-Hall}{% Anonymous:1987:BRC,% Horning:1989:BRE% }. \NAMECITE{presence}{% Chajed:2017:CFS% }. \NAMECITE{Presentation}{% Black:2012:PSD% }. \NAMECITE{Presentations}{% Baer:1965:RPP% }. \NAMECITE{presented}{% Anonymous:1976:SSE% }. \NAMECITE{Prespecification}{% Hoare:1985:WP,% Hoare:1987:PDR,% Hoare:1986:WPa,% Hoare:1986:WPb,% Hoare:1987:WP% }. \NAMECITE{Press}{% Barron:1975:BRS% }. \NAMECITE{Price}{% Barron:1975:BRS,% Horning:1989:BRE% }. \NAMECITE{Principles}{% Lenzerini:2008:PTS% }. \NAMECITE{Probabilistic}{% Barthe:2012:PRH,% Hartog:2002:VPP,% Woodcock:2019:PSR,% He:1997:LTP,% He:1999:LTP,% denHartog:2008:TMC% }. \NAMECITE{problem}{% Chisholm:1989:ARP% }. \NAMECITE{problems}{% Page:1989:SME% }. \NAMECITE{Procedure}{% BrinchHansen:2002:OCP% }. \NAMECITE{Procedures}{% Damm:1983:SRH,% Hoare:1971:PPA,% Nipkow:2002:HLR,% Fokkinga:1987:CPS,% Olderog:1983:CHL,% Olderog:1984:CPP% }. \NAMECITE{Proceedings}{% ACM:1976:SPE,% Hoare:1972:OST,% Hoare:2001:ETS,% Broy:1996:DPD,% Davies:2000:MPC,% IEEE:1988:ASL,% ACM:1983:PFA,% Abadi:2005:CCT,% Berghammer:2009:RKA,% Bottaci:2010:TAI,% Gibbons:2012:MPC,% Haddad:2012:ATP,% Hofner:2014:RAM,% IEEE:2000:PSA,% Lenzerini:2008:PTS,% Ryder:1999:PAS,% Bjorner:1990:VVZ,% Kapur:1992:ADC,% Ribeiro:2019:UTP,% Rishe:1990:PIC% }. \NAMECITE{Process}{% Brookes:2021:CPP,% Groote:1994:PAG,% Hoare:2005:PAUa,% Hoare:2005:PAUb,% Hoare:2012:LPU,% Pettersson:1991:LEC,% VanGasteren:1990:CPD,% Hoare:2014:LPU% }. \NAMECITE{Processes}{% Brookes:1984:TCS,% Dijkstra:1971:HOS,% Hoare:1978:CCS,% Hoare:1978:CSPb,% Hoare:1981:CTCb,% Hoare:1981:PCC,% Hoare:1985:CSP,% Hoare:1987:ASP,% Hoare:2002:CSP,% Hoare:2008:SLS,% Hoare:2021:CSP,% Kaubisch:1982:DES,% Olderog:1986:SOS,% Abdallah:2005:CSP,% Enikeev:1987:MTC,% Hehner:1983:MCM,% Hoare:1978:CSPa,% Hoare:1980:MCSa,% Hoare:1980:MCSb,% Hoare:1980:SPP,% Hoare:1981:CTCa,% Hoare:1981:MCS,% Hoare:1982:CCT,% Hoare:1983:NCS,% Hoare:1991:ASP,% Hoare:2011:LEL,% Josephs:1989:TAP,% Olderog:1983:SOS,% Zhou:1981:PCC,% deBoer:2002:HLD,% Hoare:1983:CSP,% Anonymous:1987:BRC% }. \NAMECITE{processing}{% Hoare:1993:PPT% }. \NAMECITE{{ProCoS}}{% Hoare:1990:AAV,% Bowen:1996:PIP% }. \NAMECITE{produce}{% Hoare:2004:FSP% }. \NAMECITE{profession}{% Hoare:1983:PEP% }. \NAMECITE{Professionalism}{% Hoare:1981:P% }. \NAMECITE{Professor}{% Davies:2000:MPC,% Dijkstra:1970:LPC,% Hoare:2016:PST% }. \NAMECITE{Program}{% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Ashcroft:1976:RPP,% Banerjee:2022:RPL,% Clint:1972:PPJ,% Fetzer:1988:PVV,% Hoare:1971:PPF,% Hoare:1975:PCP,% Hoare:1987:OSF,% Hoare:2007:IPC,% Huisman:2000:JPV,% vanAmmers:1998:PCC,% vanDiepen:1986:PDT,% Bergstra:1984:PPI,% Brotherston:2008:CPP,% Broy:1996:DPD,% Chlipala:2013:BSP,% Csirmaz:1981:PPV,% Dahl:1972:HPS,% Foley:1971:PRP,% Gibbons:2012:MPC,% Hoare:1971:PP,% Hoare:1972:PSP,% Hoare:2002:APV,% Makowsky:1989:WSO,% Neuhold:1977:UHM,% Pritchard:1979:CPJ% }. \NAMECITE{Programmers}{% Hoare:1993:MPM% }. \NAMECITE{Programming}{% Bates:1976:SPI,% BrinchHansen:2002:OCP,% Cherniavsky:1979:CCH,% Clarke:1979:PLC,% Dahl:1972:SP,% Ershov:1974:IST,% Feuer:1984:CAP,% Hoare:1969:ABC,% Hoare:1972:ADP,% Hoare:1972:TTP,% Hoare:1973:ADP,% Hoare:1973:HPLa,% Hoare:1973:HPLb,% Hoare:1973:HPLc,% Hoare:1974:ACA,% Hoare:1974:CCF,% Hoare:1983:ABC,% Hoare:1983:PEP,% Hoare:1984:PSS,% Hoare:1985:MLP,% Hoare:1986:MP,% Hoare:1992:LP,% Hoare:1993:MPM,% Hoare:1994:UTP,% Hoare:1997:UTPa,% Hoare:1997:UTPb,% Hoare:1998:UTP,% Hoare:1999:TPT,% Hoare:2001:ABC,% Hoare:2002:ABC,% Hoare:2002:APS,% Hoare:2002:TTP,% Hoare:2012:LPU,% Hoare:2013:GML,% Jones:2021:TPL,% Kaubisch:1976:QP,% Kernighan:1984:WPM,% Liu:2013:TPF,% ODonnell:1982:CFH,% Ryder:1999:PAS,% Wolff:2013:UTP,% Woodcock:2021:HHU,% Bergstra:1984:HLP,% Chlipala:2013:BSP,% Dijkstra:1972:NSP,% Dijkstra:1976:DP,% He:1990:CSP,% He:1997:LTP,% He:1999:LTP,% Hoare:1964:EAP,% Hoare:1970:BRC,% Hoare:1972:PBP,% Hoare:1973:CPE,% Hoare:1973:HLP,% Hoare:1974:ADP,% Hoare:1974:HPL,% Hoare:1975:HDP,% Hoare:1975:PPA,% Hoare:1976:HCP,% Hoare:1976:HDP,% Hoare:1976:PPA,% Hoare:1976:SPI,% Hoare:1980:HP,% Hoare:1981:TMB,% Hoare:1985:MP,% Hoare:1986:MPI,% Hoare:1987:CLP,% Hoare:1987:LP,% Hoare:1989:VPL,% Hoare:1990:AAV,% Hoare:1990:CSP,% Hoare:1996:PPA,% Hoare:2001:UTL,% Hoare:2009:VRA,% Hoare:2013:LPC,% Hoare:2013:USC,% Hoare:2014:LCP,% Hoare:2014:LPU,% Kernighan:1981:WPM,% Ni:2006:CAP,% Ribeiro:2019:UTP,% Roscoe:1986:LOP,% Roscoe:1988:LOP,% Seres:1999:ALP,% Barth:1974:BRJ,% Hoare:1996:PAB,% Barron:1975:BRS,% Lloyd:1974:BRS% }. \NAMECITE{{{programmirovanie}}}{% Dahl:1975:CSP% }. \NAMECITE{Programs}{% Bergstra:1984:ASP,% Csirmaz:1981:PPV,% Greif:1981:SSW,% Hartog:2002:VPP,% Hoare:1984:PEP,% Hoare:1984:PP,% Hoare:1985:PP,% Hoare:1993:PP,% Joseph:1987:PRF,% Lamport:1980:HLC,% Naumann:2019:WSP,% Poskitt:2012:HSV,% Bergstra:1982:SNS,% Boyer:1992:ACP,% Chisholm:1989:ARP,% Hoare:1982:SPI,% Hoare:1986:MAS,% Hoare:2008:VFG,% Hortala-Gonzalez:1989:HLN,% LeGuyadec:1996:SLP,% Lifschitz:1984:VPG,% Nanevski:2008:YDT,% Naumann:1995:PTH,% Nielson:1987:HLP,% Olderog:1983:CHL,% Olderog:1984:CPP,% Shaner:2007:MVH,% Shapiro:2006:PPC,% Stoller:1995:VPU,% Ying:2011:FHL% }. \NAMECITE{Progress}{% Guttmann:2019:CFC% }. \NAMECITE{Project}{% Hoare:2008:VST,% Bowen:1996:PIP,% Mller:2021:FFY% }. \NAMECITE{Proof}{% Foley:1971:PRP,% Hoare:1971:PP,% Hoare:1971:PPF,% Hoare:1972:PCD,% Hoare:1972:PSP,% Hoare:1976:PCD,% Hoare:1996:HDS,% Hoare:2001:PCD,% Hoare:2002:PCD,% Joseph:1987:PRF,% Sokolowski:1987:SHL,% DeBoer:1997:HSC,% Fokkinga:1987:CPS,% He:1987:ASP,% Hoare:1986:ASP,% Hoare:1987:DPM,% Hoare:1991:DPM,% Kapur:1994:OTP,% Nielson:1987:HLP,% VanGasteren:1990:CPD,% Verjus:1987:PDA,% Hoare:1996:PPC% }. \NAMECITE{Proofs}{% Barthe:2012:PRH,% Hoare:1987:ASP,% Barthe:2009:FCC,% Boyer:1992:ACP,% Boyer:1996:APO,% Brotherston:2008:CPP,% Gardiner:1995:APC,% Hoare:1975:PCP,% Hoare:1991:ASP,% LeGuyadec:1996:SLP,% Shapiro:2006:PPC,% denHartog:2008:TMC% }. \NAMECITE{Properties}{% Hoare:1978:SPP,% Hoare:1986:ASP,% Sousa:2016:CHL% }. \NAMECITE{propositional}{% Cohen:2000:NCP,% Hoare:1985:CNP% }. \NAMECITE{Prospects}{% Hoare:1972:PBP% }. \NAMECITE{Protocols}{% Hoare:1981:PCC% }. \NAMECITE{prototyping}{% Hoare:1990:AAV% }. \NAMECITE{{protsessy}}{% Khoar:1989:CVC% }. \NAMECITE{Provably}{% He:1994:PCS% }. \NAMECITE{proves}{% Hoare:1990:RAPa,% Hoare:1990:RAPb,% Hoare:1992:RAP% }. \NAMECITE{Proving}{% Ashcroft:1976:RPP,% Bergstra:1984:PPI,% Clint:1972:PPJ,% Vafeiadis:2006:PCH,% Chisholm:1989:ARP,% Hoare:2010:TPH% }. \NAMECITE{Publications}{% Baer:1965:RPP,% Jones:2021:LTH% }. \NAMECITE{purpose}{% Hoare:1972:OSTb% }. \NAMECITE{Qatar}{% Berghammer:2009:RKA% }. \NAMECITE{quality}{% Hoare:1972:GEQ% }. \NAMECITE{Quantum}{% Feng:2021:QHL,% Ying:2011:FHL% }. \NAMECITE{Quasiparallel}{% Kaubisch:1976:QP% }. \NAMECITE{Queen}{% Hoare:1972:OST,% Hoare:1971:CSI% }. \NAMECITE{quest}{% Hoare:2003:KTK% }. \NAMECITE{Question}{% Lewis:1997:BCI% }. \NAMECITE{questions}{% RodriguezArtalejo:1985:SQA% }. \NAMECITE{queueing}{% Hoare:1973:GCL% }. \NAMECITE{quick}{% Pritchard:1979:CPJ% }. \NAMECITE{quick-sort}{% Pritchard:1979:CPJ% }. \NAMECITE{{Quickselect}}{% Prodinger:1995:MQH% }. \NAMECITE{Quicksort}{% JaJa:2000:PQ,% Foley:1971:PRP,% Fouz:2012:SAQ,% Hoare:1961:AQ,% Hoare:1962:Q,% Hoare:1996:PQ,% Neuhold:1977:UHM% }. \NAMECITE{R}{% Anonymous:1987:BRC,% Ashcroft:1976:RPP,% Baer:1965:RPP,% Barron:1975:BRS,% Barth:1974:BRJ,% Brockhaus:1973:BRC,% Dijkstra:1970:LPC,% Dijkstra:1974:LCR,% Dijkstra:1975:VTO,% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa,% Dijkstra:1982:PTP,% Dijkstra:1982:VTO,% Dijkstra:20xx:ERC,% Hoare:1982:VTO,% Horning:1989:BRE,% Jones:2010:RWC,% Lloyd:1974:BRS,% Roscoe:1994:CME,% Shustek:2009:IIC% }. \NAMECITE{{R.}}{% Pritchard:1979:CPJ% }. \NAMECITE{RAMiCS}{% Hofner:2014:RAM% }. \NAMECITE{{Randell}}{% Jones:2011:DHC% }. \NAMECITE{reactive}{% DeBoer:1997:HSC% }. \NAMECITE{Real}{% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Hooman:1992:CVR,% Hoare:1975:HDP,% Hoare:1976:HDP,% Hooman:1994:EHL% }. \NAMECITE{Real-Time}{% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Hooman:1992:CVR,% Hoare:1975:HDP,% Hoare:1976:HDP,% Hooman:1994:EHL% }. \NAMECITE{Realizations}{% Reus:2001:HCV% }. \NAMECITE{Reasoning}{% Shankar:1993:IAR,% deBoer:2021:CCR,% vonHenke:1985:RHS,% Chisholm:1989:ARP,% Delbianco:2013:HSR,% Gardner:2008:LHR,% Gordon:1992:MRH,% Pettersson:1991:LEC,% Turon:2013:URH% }. \NAMECITE{receipt}{% Hoare:2012:MT,% Hoare:2012:MTR% }. \NAMECITE{Recommendation}{% Hoare:1968:RDR% }. \NAMECITE{Record}{% Hoare:1965:RH,% Hoare:1968:RH,% Dijkstra:20xx:ERC% }. \NAMECITE{Recovery}{% Hoare:2011:RB,% He:1987:ASP% }. \NAMECITE{Recursion}{% Mamouras:2016:HLD% }. \NAMECITE{Recursive}{% Hoare:1975:RDS,% Nipkow:2002:HLR,% Foley:1971:PRP% }. \NAMECITE{Reduction}{% Johnston:1975:MRE% }. \NAMECITE{redundant}{% Mancini:1988:HLD% }. \NAMECITE{reference}{% Spivey:1989:ZNR% }. \NAMECITE{refined}{% He:1986:DRR% }. \NAMECITE{Refinement}{% Hoare:1990:RAPa,% Hoare:1990:RAPb,% Hoare:1992:RAP,% He:1986:DRR,% He:1990:DRC,% Hoare:1987:PDR,% Hoare:1990:DRC,% Turon:2013:URH% }. \NAMECITE{refinements}{% vanAmmers:1998:PCC% }. \NAMECITE{Reflections}{% Jones:2010:RWC% }. \NAMECITE{regular}{% Hortala-Gonzalez:1989:HLN% }. \NAMECITE{relation}{% Gritzner:1996:RAM% }. \NAMECITE{Relational}{% Banerjee:2022:RPL,% Barthe:2012:PRH,% Berghammer:2009:RKA,% Hofner:2014:RAM% }. \NAMECITE{Relations}{% Berghammer:2009:RKA,% Foster:2019:HRI% }. \NAMECITE{relative}{% RodriguezArtalejo:1985:SQA% }. \NAMECITE{Relatively}{% Damm:1983:SRH% }. \NAMECITE{Reliability}{% Broy:2007:SSR,% Hoare:1975:DR% }. \NAMECITE{Reliable}{% Hoare:1996:HDS% }. \NAMECITE{RelMiCS}{% Berghammer:2009:RKA% }. \NAMECITE{Rely}{% Hayes:2019:DAR% }. \NAMECITE{Rely/Guarantee}{% Hayes:2019:DAR% }. \NAMECITE{Remark}{% Brown:1976:RAA% }. \NAMECITE{Remarks}{% Ashcroft:1976:RPP% }. \NAMECITE{Remote}{% BrinchHansen:2002:OCP% }. \NAMECITE{Report}{% Bates:1976:SPI,% Dijkstra:1970:NIM,% Hoare:1962:REA,% Hoare:1968:RDR,% Woodger:1969:MRA,% Bowen:1996:PIP% }. \NAMECITE{repository}{% Bicarregui:2006:VSR% }. \NAMECITE{Representations}{% Hoare:2001:PCD,% Hoare:2002:PCD,% Hoare:1972:PCD,% Hoare:1976:PCD,% Hoare:1996:PPC% }. \NAMECITE{Reprint}{% Hoare:1983:ABC,% Hoare:1983:CSP% }. \NAMECITE{Research}{% Bottaci:2010:TAI,% Hoare:2003:VCGa,% Hoare:2004:GCC,% Hoare:2005:GCC,% Bowen:1996:PIP,% Cleaveland:1996:SDC,% Hoare:2003:VCGb,% Hoare:2005:VCG% }. \NAMECITE{Researcher}{% Anonymous:20xx:THE% }. \NAMECITE{Resources}{% Gray:2021:OR% }. \NAMECITE{Responses}{% Anonymous:2007:DIPb% }. \NAMECITE{Result}{% Wand:1978:NIR,% Wand:1976:NIR% }. \NAMECITE{resume}{% He:1986:DRR% }. \NAMECITE{retract}{% He:2010:CRC% }. \NAMECITE{Retrospective}{% Hoare:2009:VRA% }. \NAMECITE{Review}{% Anonymous:1987:BRC,% Barron:1975:BRS,% Barth:1974:BRJ,% Hoare:1970:BR,% Hoare:1970:BRC,% Hoare:1977:BR,% Horning:1989:BRE,% Lloyd:1974:BRS,% Brockhaus:1973:BRC,% Hoare:1964:BRA% }. \NAMECITE{Reviews}{% Hoare:1963:BR% }. \NAMECITE{Revised}{% Abdallah:2005:CSP,% Meyer:2008:VST,% Wolff:2013:UTP% }. \NAMECITE{Revisited}{% vonOheimb:2002:HLN,% Kirkerud:1982:CHC% }. \NAMECITE{Rewriting}{% Jones:2001:PRR,% Sun:1996:TRH% }. \NAMECITE{Richard}{% Black:2012:PSD,% Dijkstra:1999:FWT,% Frana:2002:ICA% }. \NAMECITE{{RoboChart}}{% Woodcock:2019:PSR% }. \NAMECITE{robust}{% Gritzner:1996:RAM% }. \NAMECITE{{Roger}}{% Herbert:2004:CST,% Hoare:2004:RMN% }. \NAMECITE{role}{% Hoare:1973:TMR% }. \NAMECITE{Roles}{% Borgstrom:2011:RSH% }. \NAMECITE{Royal}{% Dijkstra:1982:PTP,% Gordon:1992:MRH% }. \NAMECITE{rule}{% Olderog:1983:NER,% Takaoka:1987:DRH% }. \NAMECITE{Rules}{% Joseph:1987:PRF,% Olderog:1981:SCH,% Cocco:1982:MEH,% Jones:2001:PRR,% Thielecke:2006:FRA% }. \NAMECITE{Running}{% Butler:2005:TSL% }. \NAMECITE{Safety}{% Broy:2011:SSS,% Hoare:1986:MAS,% Sousa:2016:CHL% }. \NAMECITE{Said}{% McReynolds:1997:LBS% }. \NAMECITE{Salute}{% Feijen:1990:BOB% }. \NAMECITE{San}{% Abadi:2005:CCT% }. \NAMECITE{Sanderson}{% Hoare:1970:BRC% }. \NAMECITE{Saratoga}{% Kapur:1992:ADC% }. \NAMECITE{Schemes}{% Mamouras:2016:HLD% }. \NAMECITE{School}{% Hoare:2001:ETS,% Bauer:1976:LHI,% Johnston:1975:MRE,% Muller:2010:ALS% }. \NAMECITE{Science}{% Hoare:1976:CST,% Hoare:1984:PSS,% Hoare:1989:ECS,% Hoare:1996:UTC,% Hoare:2001:ETS,% Hoare:2007:SEC,% Hofner:2014:RAM,% IEEE:1976:ASF,% IEEE:1988:ASL,% Berghammer:2009:RKA,% Davies:2000:MPC,% Hoare:1971:CSI,% Hoare:1996:MMC,% Hoare:1998:SCE,% Horning:1989:BRE% }. \NAMECITE{Sciences}{% Hoare:2001:ETS% }. \NAMECITE{Scientific}{% Elliott:1989:SAM,% Hoare:2002:APS% }. \NAMECITE{Scientists}{% Hoare:1989:NAC% }. \NAMECITE{scope}{% Hoare:1972:OSTb% }. \NAMECITE{{Scotland}}{% IEEE:1988:ASL% }. \NAMECITE{sd\&m}{% Broy:2001:PTC% }. \NAMECITE{second}{% Makowsky:1989:WSO% }. \NAMECITE{Security}{% Barthe:2012:PRH,% Broy:2007:SSR% }. \NAMECITE{SELECT}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{Selected}{% Dijkstra:1982:SWC,% Meyer:2008:VST,% Wolff:2013:UTP% }. \NAMECITE{Selection}{% Grubel:1996:ADT,% Grubel:1998:HSA% }. \NAMECITE{self}{% Cai:2007:CSM% }. \NAMECITE{self-modifying}{% Cai:2007:CSM% }. \NAMECITE{Semantical}{% Pratt:1976:SCF% }. \NAMECITE{Semantics}{% Aichernig:2019:TPA,% Bergstra:1984:ASP,% Butler:2005:TSL,% Francez:1978:SNC,% Francez:1979:SNC,% Greif:1981:SSW,% Hoare:1974:CCF,% Hoare:1994:ACO,% Hoare:2005:TSO,% Hoare:2008:SLS,% Olderog:1986:SOS,% PeytonJones:1999:SIE,% Woodcock:2019:PSR,% Wu:2019:USC,% He:1990:CSP,% He:1993:AOS,% Hoare:1990:CSP,% Hoare:1997:ADO,% Hoare:2000:ADO,% Hoare:2013:USC,% Jones:1999:SIE,% Olderog:1983:SOS,% Saabas:2007:CNS,% Tennent:1991:CPW% }. \NAMECITE{Semaphores}{% BrinchHansen:2002:OCP% }. \NAMECITE{Seminar}{% Hoare:1972:OST% }. \NAMECITE{Sentences}{% Hoare:1961:MSS,% vonHenke:1985:RHS% }. \NAMECITE{Separation}{% Hoare:2008:SLS,% Brotherston:2008:CPP,% Nanevski:2006:PSH,% Nanevski:2008:HTT,% Wehrman:2009:GMS% }. \NAMECITE{September}{% Anonymous:1976:SSE,% Bottaci:2010:TAI,% Hoare:1972:OST,% Jones:2013:ICC,% Pettersson:1991:LEC% }. \NAMECITE{Sequential}{% Anonymous:1987:BRC,% Brookes:1984:TCS,% Dijkstra:1971:HOS,% Hoare:1978:CCS,% Hoare:1978:CSPb,% Hoare:1983:CSP,% Hoare:1985:CSP,% Hoare:1986:NCS,% Hoare:1987:ASP,% Hoare:2002:CSP,% Hoare:2021:CSP,% Kaubisch:1982:DES,% LeGuyadec:1996:SLP,% vonKarger:1995:SC,% Abdallah:2005:CSP,% Enikeev:1987:MTC,% Hoare:1978:CSPa,% Hoare:1980:MCSa,% Hoare:1980:MCSb,% Hoare:1981:MCS,% Hoare:1983:NCS,% Hoare:1985:NCS,% Hoare:1991:ASP,% Zhou:1981:PCC% }. \NAMECITE{Sequential-like}{% LeGuyadec:1996:SLP% }. \NAMECITE{Series}{% Hoare:2001:ETS% }. \NAMECITE{service}{% Hoare:1985:SSN,% Hoare:1986:ASP,% Hoare:1987:DPM,% Hoare:1991:DPM,% Morgan:1985:SSN% }. \NAMECITE{Set}{% Hoare:1968:SM% }. \NAMECITE{setting}{% Csirmaz:1981:PPV,% He:1990:DRC,% Hoare:1990:DRC% }. \NAMECITE{Seventh}{% IEEE:2000:PSA,% Lenzerini:2008:PTS% }. \NAMECITE{several}{% Prodinger:1995:MQH% }. \NAMECITE{shared}{% DeBoer:1997:HSC% }. \NAMECITE{shifts}{% Hoare:2004:FSP% }. \NAMECITE{Side}{% vonOheimb:2002:HLN% }. \NAMECITE{sieve}{% Hoare:1972:PSP% }. \NAMECITE{SIGACT}{% Lenzerini:2008:PTS% }. \NAMECITE{SIGART}{% Lenzerini:2008:PTS% }. \NAMECITE{SIGMOD}{% Lenzerini:2008:PTS% }. \NAMECITE{SIGMOD-SIGACT-SIGART}{% Lenzerini:2008:PTS% }. \NAMECITE{SIGPLAN}{% Hoare:2012:MT,% Ryder:1999:PAS,% Black:2012:PSD,% Hoare:2012:MTR% }. \NAMECITE{Simple}{% Cherniavsky:1979:CCH% }. \NAMECITE{simplified}{% Hoare:1985:SSN,% Morgan:1985:SSN% }. \NAMECITE{Simulation}{% Engelhardt:1996:SSS,% Kaubisch:1982:DES% }. \NAMECITE{{Simulink}}{% Zhan:2019:UGC% }. \NAMECITE{{Simulink/Stateflow}}{% Zhan:2019:UGC% }. \NAMECITE{Single}{% Hoare:1966:SPC% }. \NAMECITE{Sir}{% Davies:2000:MPC,% Hoare:2016:PST,% Black:2012:PSD,% Dale:1994:CST% }. \NAMECITE{size}{% Hoare:1974:OSS% }. \NAMECITE{Smallest}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{Smoothed}{% Fouz:2012:SAQ% }. \NAMECITE{{Smyth}}{% Flannery:1990:HSP% }. \NAMECITE{Society}{% Gordon:1992:MRH,% Dijkstra:1982:PTP% }. \NAMECITE{Software}{% Beckert:2006:ISF,% Broy:2001:PTC,% Broy:2002:SPC,% Broy:2003:MAL,% Broy:2005:ETS,% Broy:2007:SSR,% Broy:2011:SSS,% Daylight:2012:DSE,% Hayes:2021:SS,% Hoare:1974:SDP,% Hoare:1975:SE,% Hoare:1978:ESS,% Hoare:1978:SEK,% Hoare:1994:HSCa,% Hoare:1996:HDS,% Hoare:2001:ETS,% Hoare:2008:VST,% Hoare:2021:PSI,% Hoare:2021:VSI,% IEEE:2000:PSA,% IEEE:2002:AIC,% Meyer:2008:VST,% Mller:2021:FFY,% Bicarregui:2006:VSR,% Bjorner:1990:VVZ,% Hoare:1972:GEQ,% Hoare:1993:WSE,% Hoare:1994:HSCb,% Hoare:1998:SCE,% Hoare:2002:AMS,% Hoare:2006:IVS,% Hoare:2009:PSI,% Hoare:2009:VSI,% Muller:2010:ALS,% Rehof:2010:ADS,% Anonymous:1976:SSE% }. \NAMECITE{solution}{% Page:1989:SME% }. \NAMECITE{Solutions}{% Dijkstra:1982:MSMa,% Dijkstra:1977:MSM% }. \NAMECITE{Some}{% Bergstra:1982:SNS,% Hoare:1978:SPP,% Hoare:1987:OSF,% RodriguezArtalejo:1985:SQA% }. \NAMECITE{Sorcery}{% Hoare:1984:PSS% }. \NAMECITE{Sorry}{% Santini:2005:WSI% }. \NAMECITE{sort}{% Pritchard:1979:CPJ% }. \NAMECITE{sorting}{% Fokkinga:1987:CPS% }. \NAMECITE{Sound}{% Damm:1983:SRH,% Olderog:1981:SCH,% Arthan:2009:GFS,% Bergstra:1982:SNS,% Hoare:2004:FSP% }. \NAMECITE{Soundness}{% Sokolowski:1987:SHL% }. \NAMECITE{Space}{% Hoare:2019:CST,% Hoare:2019:CSTa% }. \NAMECITE{Spain}{% Gibbons:2012:MPC% }. \NAMECITE{Special}{% Hoare:2021:PSI,% Hoare:2009:PSI% }. \NAMECITE{Specific}{% Enslow:1975:ILRc% }. \NAMECITE{Specification}{% Broy:2011:SSS,% Hayes:2021:SS,% Hoare:1985:SSN,% Morgan:1985:SSN,% Olderog:1983:SOS,% Olderog:1986:SOS,% Engelhardt:1996:SSS,% He:1987:ASP,% Hoare:1986:ASP,% Hoare:1990:AAV,% Rehof:2010:ADS% }. \NAMECITE{Specification-Oriented}{% Olderog:1986:SOS,% Olderog:1983:SOS% }. \NAMECITE{Specifications}{% Hoare:1982:SPI,% Hoare:1987:ASP,% Naumann:2019:WSP,% Hoare:1990:RAPa,% Hoare:1990:RAPb,% Hoare:1991:ASP,% Sergey:2016:HSS% }. \NAMECITE{specified}{% Shaner:2007:MVH% }. \NAMECITE{Specifying}{% Greif:1981:SSW% }. \NAMECITE{spheres}{% Hoare:2004:FSP% }. \NAMECITE{Springs}{% Kapur:1992:ADC% }. \NAMECITE{stacks}{% Borgstrom:2011:RSH% }. \NAMECITE{standard}{% Xu:2016:CHL% }. \NAMECITE{{Standardisation}}{% Enslow:1975:ILRa% }. \NAMECITE{Startling}{% Hoare:1978:ESS% }. \NAMECITE{State}{% Bates:1976:SPI,% Becker:2010:LSM% }. \NAMECITE{state-modifying}{% Becker:2010:LSM% }. \NAMECITE{{Stateflow}}{% Zhan:2019:UGC% }. \NAMECITE{Statement}{% Hoare:1972:NS,% Hoare:1996:UTP% }. \NAMECITE{statements}{% Engelhardt:1996:SSS,% Lifschitz:1984:VPG% }. \NAMECITE{step}{% Bicarregui:2006:VSR% }. \NAMECITE{{STOC}}{% ACM:1976:SPE% }. \NAMECITE{store}{% Hoare:1968:DST,% Hoare:1972:SSMa,% Hoare:1972:SSMb,% Hoare:1974:OSS% }. \NAMECITE{Stories}{% Hoare:2000:SLI% }. \NAMECITE{Story}{% Hoare:1991:TOP% }. \NAMECITE{Strategic}{% Cleaveland:1996:SDC% }. \NAMECITE{Strict}{% Guttmann:2019:CFC% }. \NAMECITE{Structure}{% Hoare:1982:SOS,% Hoare:1976:SOS% }. \NAMECITE{Structured}{% Barth:1974:BRJ,% Bates:1976:SPI,% Dahl:1972:SP,% Hoare:1976:SPI,% Chlipala:2013:BSP,% Dijkstra:1972:NSP,% Hoare:1972:PSP,% Hoare:1973:SPS,% Barron:1975:BRS,% Lloyd:1974:BRS% }. \NAMECITE{structures}{% Bergstra:1982:SNS,% Dahl:1972:HPS,% Hoare:1968:DST,% Hoare:1975:RDS% }. \NAMECITE{Structuring}{% Hoare:1974:MOS,% Hoare:2002:MOS,% Hoare:1972:NDS% }. \NAMECITE{Strukturnoe}{% Dahl:1975:CSP% }. \NAMECITE{Stuck}{% Fournet:2004:SFC% }. \NAMECITE{Stuck-free}{% Fournet:2004:SFC% }. \NAMECITE{Student}{% Jones:2013:ICC% }. \NAMECITE{Students}{% Jones:2021:DS% }. \NAMECITE{{Studer}}{% Pritchard:1979:CPJ% }. \NAMECITE{Study}{% Broy:1996:DPD,% Hoare:2010:MJD% }. \NAMECITE{stvuyushchie}{% Khoar:1989:CVC% }. \NAMECITE{Style}{% ODonnell:1982:CFH,% Poskitt:2012:HSV,% DeBoer:1997:HSC,% Delbianco:2013:HSR,% Sergey:2016:HSS,% Turon:2013:URH,% denHartog:2008:TMC% }. \NAMECITE{substitution}{% Rehof:2010:ADS% }. \NAMECITE{Success}{% Apt:2021:ASI,% Gozum:1997:LWC% }. \NAMECITE{suggested}{% Dijkstra:20xx:ERC% }. \NAMECITE{Summer}{% Hoare:2001:ETS,% Bauer:1976:LHI,% Muller:2010:ALS% }. \NAMECITE{Survey}{% Apt:1981:TYH,% Apt:1984:TYH,% Hoare:1972:SSMa,% Hoare:1972:SSMb% }. \NAMECITE{sweet}{% Hoare:2004:FSP% }. \NAMECITE{switching}{% Hoare:1988:PCC,% Hoare:1990:MSS,% Zhou:1992:MSS% }. \NAMECITE{Switzerland}{% Meyer:2008:VST% }. \NAMECITE{Symposium}{% ACM:1983:PFA,% Bjorner:1990:VVZ,% Davies:2000:MPC,% Ershov:1974:IST,% IEEE:1976:ASF,% IEEE:1988:ASL,% Lenzerini:2008:PTS,% Ribeiro:2019:UTP,% Wolff:2013:UTP,% ACM:1976:SPE,% Abdallah:2005:CSP% }. \NAMECITE{Synchronisation}{% Hoare:1980:SPP% }. \NAMECITE{synchronous}{% Hoare:1990:MSS,% Zhou:1992:MSS% }. \NAMECITE{synchrony}{% He:1990:TSA% }. \NAMECITE{Syntagmatic}{% Hoare:1961:MSS% }. \NAMECITE{Synthesizing}{% Hoare:1961:MSS% }. \NAMECITE{System}{% Broy:2007:SSR,% Hoare:1974:MOS,% Hoare:1982:SOS,% Hoare:2002:MOS,% Qian:1990:ASD,% Wand:1978:NIR,% Chajed:2017:CFS,% Chlipala:2013:BSP,% Hoare:1963:EAI,% Hoare:1964:EAP,% Hoare:1973:SPS,% Hoare:1976:SOS,% Hoare:1989:FMC,% Kapur:1994:OTP,% Nielson:1987:HLP,% Szczepanska:1991:HLV,% Wand:1976:NIR% }. \NAMECITE{Systems}{% Beckert:2006:ISF,% Brockhaus:1973:BRC,% Broy:2005:ETS,% Broy:2011:SSS,% Clarke:1979:PLC,% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% He:1994:PCS,% Herbert:2004:CST,% Hoare:1972:OST,% Hoare:1986:NCS,% Hoare:2001:ETS,% Hooman:1992:CVR,% Lenzerini:2008:PTS,% Shankar:1993:IAR,% Zhan:2019:UGC,% Anonymous:1976:SSE,% Arthan:2013:HLL,% DeBoer:1997:HSC,% Enikeev:1987:MTC,% Hoare:1972:OSTb,% Hoare:1985:NCS,% Makowsky:1989:WSO,% Mancini:1988:HLD,% Rehof:2010:ADS,% Ridge:2009:VDS% }. \NAMECITE{TAIC}{% Bottaci:2010:TAI% }. \NAMECITE{talk}{% Hoare:2000:LC,% Hoare:2006:IVS% }. \NAMECITE{Tame}{% Struth:2021:THA% }. \NAMECITE{Tasks}{% Hoare:1993:MPM% }. \NAMECITE{TC}{% Meyer:2008:VST% }. \NAMECITE{Teaching}{% Sufrin:2021:TBO% }. \NAMECITE{Tears}{% Macnaghten:1977:FFT% }. \NAMECITE{technique}{% Hoare:2010:MJD,% Jones:2001:PRR% }. \NAMECITE{Techniques}{% Bottaci:2010:TAI,% Hoare:1972:OST,% Hoare:1972:SSMa,% Hoare:1972:SSMb,% Brockhaus:1973:BRC% }. \NAMECITE{Technology}{% Herbert:2004:CST,% Hoare:1976:CST,% Hoare:1983:TF% }. \NAMECITE{{Tecton}}{% Kapur:1994:OTP% }. \NAMECITE{Ten}{% Apt:1981:TYH,% Apt:1984:TYH,% McReynolds:1997:LBS% }. \NAMECITE{Term}{% Sun:1996:TRH% }. \NAMECITE{Termination}{% Huisman:2000:JPV,% Brotherston:2008:CPP% }. \NAMECITE{Testing}{% Aichernig:2019:TPA,% Hoare:2010:TPH,% Bottaci:2010:TAI% }. \NAMECITE{tests}{% Kozen:2000:HLK% }. \NAMECITE{Texas}{% IEEE:1976:ASF% }. \NAMECITE{text}{% Woodger:1969:MRA% }. \NAMECITE{th}{% Brown:1976:RAA,% Floyd:1975:AAA% }. \NAMECITE{thanks}{% Hoare:2012:MT,% Hoare:2012:MTR% }. \NAMECITE{Their}{% Broy:2001:PTC,% Bergstra:1982:SNS,% Hoare:1972:OSTb,% Hoare:1976:CST,% Rishe:1990:PIC% }. \NAMECITE{Theme}{% Hoare:1982:VTO,% Dijkstra:1975:VTO,% Dijkstra:1982:VTO% }. \NAMECITE{Theorems}{% Bergstra:1982:TTA% }. \NAMECITE{Theoretical}{% Ershov:1974:IST,% Hoare:1993:PPT% }. \NAMECITE{Theories}{% Baeten:1990:CTC,% Bloom:1991:FHL,% Broy:2005:ETS,% Hoare:1974:CCF,% Hoare:1994:UTP,% Hoare:1996:UTC,% Hoare:1997:UTPa,% Hoare:1997:UTPb,% Hoare:1998:UTP,% Hoare:1999:TPT,% Hoare:2001:ETS,% Hoare:2008:VST,% Jones:2021:TPL,% Liu:2013:TPF,% Meyer:2008:VST,% Wolff:2013:UTP,% Woodcock:2021:HHU,% He:1997:LTP,% He:1999:LTP,% He:2000:UTH,% He:2005:LTC,% Hoare:1996:UTP,% Hoare:1997:UTC,% Hoare:2001:UTL,% Ribeiro:2019:UTP% }. \NAMECITE{Theory}{% ACM:1976:SPE,% ACM:1983:PFA,% Baer:1965:RPP,% Bazilevskii:1963:TMM,% Brookes:1984:TCS,% Grubel:1996:ADT,% Haddad:2012:ATP,% Herbert:2004:CST,% Hoare:1972:TTP,% Hoare:1989:NAC,% Hoare:2002:APS,% Hoare:2002:TTP,% Abadi:2005:CCT,% Enikeev:1987:MTC,% He:1990:TSA,% Hoare:1980:TND,% Hoare:1990:MSS,% Hoare:1990:TCC,% Hoare:1990:TDC,% Hoare:1991:TCC,% Hoare:1991:TDCa,% Hoare:1991:TDCb,% Hoare:2010:MJD,% Josephs:1989:TAP,% Kennaway:1980:TN,% Nanevski:2006:PSH,% Nanevski:2008:HTT,% Zhou:1992:MSS% }. \NAMECITE{there}{% Hoare:1981:TMB% }. \NAMECITE{think}{% Hoare:2004:YWT% }. \NAMECITE{Third}{% Bjorner:1990:VVZ,% Hoare:2007:IPC% }. \NAMECITE{thousand}{% Dijkstra:1999:FWT% }. \NAMECITE{Time}{% Enslow:1975:ILRa,% Enslow:1975:ILRb,% Enslow:1975:ILRc,% Hoare:2019:CST,% Hooman:1992:CVR,% Manna:2010:TVE,% Hoare:1975:HDP,% Hoare:1976:HDP,% Hoare:2019:CSTa,% Hooman:1994:EHL,% Nielson:1987:HLP% }. \NAMECITE{times}{% Hoare:2000:SLI% }. \NAMECITE{timetables}{% Johnston:1975:MRE% }. \NAMECITE{Tolerant}{% Joseph:1987:PRF% }. \NAMECITE{Tomorrow}{% Hoare:1973:TMR% }. \NAMECITE{Tony}{% Hoare:2016:PST,% Ribeiro:2019:UTP,% Anonymous:2007:DIPa,% Anonymous:2007:DIPb,% Anonymous:20xx:THE,% Daylight:2012:THM,% Dijkstra:1989:ETH,% Jones:2021:LTH,% Jones:2021:TPL% }. \NAMECITE{Tools}{% Hoare:2008:VST,% Meyer:2008:VST% }. \NAMECITE{Top}{% Cipra:2000:BCE,% Hoare:1999:TPT% }. \NAMECITE{Top-Down}{% Hoare:1999:TPT% }. \NAMECITE{toppled}{% Hoare:2003:KTK% }. \NAMECITE{Total}{% Hoare:1981:CTCb,% Hoare:1981:CTCa,% Hoare:1982:CCT% }. \NAMECITE{Trace}{% Butler:2005:TSL,% Hoare:1999:TMPb,% Hoare:1999:TMPa% }. \NAMECITE{Transactions}{% Butler:2005:TSL,% Hoare:2007:CT,% Hoare:2010:CT,% Qian:1990:ASD% }. \NAMECITE{Transform}{% Macnaghten:1977:FFT% }. \NAMECITE{Transformations}{% vanDiepen:1986:PDT% }. \NAMECITE{Transformers}{% Hoare:1978:SPP,% Dijkstra:1982:PTP,% Naumann:1995:PTH% }. \NAMECITE{Translation}{% Hoare:1961:MSS% }. \NAMECITE{translator}{% Hoare:1962:REA% }. \NAMECITE{Transputer}{% Hoare:1991:TOP% }. \NAMECITE{{Traub}}{% Dijkstra:1977:MSM,% Dijkstra:1982:MSMa% }. \NAMECITE{Tree}{% Hoare:2005:TSO% }. \NAMECITE{tribute}{% Herbert:2004:CST% }. \NAMECITE{Trick}{% Hoare:2010:UCT% }. \NAMECITE{Trimming}{% Struth:2021:THA% }. \NAMECITE{triple}{% Borgstrom:2011:RSH% }. \NAMECITE{Triples}{% Hooman:1992:CVR% }. \NAMECITE{true}{% Pettersson:1991:LEC,% VanGasteren:1990:CPD% }. \NAMECITE{{Tuesday}}{% Dijkstra:1982:PTP% }. \NAMECITE{Turing}{% Ashenhurst:1987:ATA,% Hoare:2016:PST,% Hoare:2021:ATA,% Daylight:2012:DSE% }. \NAMECITE{Tutorial}{% Greif:1981:SSW% }. \NAMECITE{Twenty}{% Lenzerini:2008:PTS,% Ashenhurst:1987:ATA% }. \NAMECITE{Twenty-Seventh}{% Lenzerini:2008:PTS% }. \NAMECITE{Two}{% Bergstra:1982:TTA,% Bergstra:1984:HLP,% Bruni:2005:CTA,% Hoare:1968:DST% }. \NAMECITE{two-level}{% Hoare:1968:DST% }. \NAMECITE{Type}{% Damm:1983:SRH,% Nanevski:2006:PSH,% Nanevski:2008:HTT% }. \NAMECITE{types}{% Bergstra:1984:HLP,% Nanevski:2008:YDT,% Thielecke:2006:FRA,% Wing:1989:VAD% }. \NAMECITE{UK}{% Abdallah:2005:CSP,% Bottaci:2010:TAI% }. \NAMECITE{Unbounded}{% Nipkow:2002:HLR% }. \NAMECITE{uncertainty}{% Hoare:2002:LLU% }. \NAMECITE{Unification}{% Baeten:1990:CTC,% Hoare:1996:UTC% }. \NAMECITE{Unified}{% Butterfield:2019:IOA,% Hoare:1994:UTP,% Hoare:1997:UTPa,% Zhan:2019:UGC% }. \NAMECITE{Unifies}{% vanStaden:2013:AUO% }. \NAMECITE{Unify}{% Hoare:2012:LPU,% Hoare:2014:LPU% }. \NAMECITE{Unifying}{% He:2000:UTH,% Hoare:1996:UTP,% Hoare:1997:UTC,% Hoare:1997:UTPb,% Hoare:1998:UTP,% Hoare:2001:UTL,% Hoare:2005:PAUa,% Hoare:2005:PAUb,% Hoare:2011:UMD,% Hoare:2013:USC,% Turon:2013:URH,% Wolff:2013:UTP,% Woodcock:2021:HHU,% Ribeiro:2019:UTP% }. \NAMECITE{United}{% Horning:1989:BRE,% Jones:2013:ICC% }. \NAMECITE{universe}{% Hoare:2004:VIF% }. \NAMECITE{University}{% Hoare:1971:CSI,% Hoare:1972:OST,% Hoare:1973:TMR,% Hoare:1986:MPI% }. \NAMECITE{Unraveling}{% Hoare:2010:UCT% }. \NAMECITE{USA}{% Abadi:2005:CCT,% Kapur:1992:ADC% }. \NAMECITE{use}{% Dasgupta:1984:UHL,% Neuhold:1977:UHM,% Pritchard:1979:CPJ,% Stoller:1995:VPU% }. \NAMECITE{used}{% Boyer:1996:APO% }. \NAMECITE{Using}{% Hartog:2002:VPP,% Hooman:1992:CVR,% Sokolowski:1987:SHL,% Zhan:2019:UGC,% Bergstra:1984:PPI,% Chajed:2017:CFS,% Chisholm:1989:ARP% }. \NAMECITE{UTP}{% Ribeiro:2019:UTP,% Wolff:2013:UTP,% Foster:2019:HRI,% Wu:2019:USC% }. \NAMECITE{Value}{% deBoer:2021:CCR% }. \NAMECITE{Vancouver}{% Lenzerini:2008:PTS% }. \NAMECITE{variable}{% DeBoer:1997:HSC% }. \NAMECITE{Variables}{% Feng:2021:QHL,% Kleymann:1999:HLA,% vonOheimb:2002:HLN,% Olderog:1984:CPP% }. \NAMECITE{Variations}{% Dijkstra:1975:VTO,% Dijkstra:1982:VTO,% Hoare:1982:VTO% }. \NAMECITE{varieties}{% Hoare:1989:VPL% }. \NAMECITE{various}{% Makowsky:1989:WSO% }. \NAMECITE{VDM}{% Bjorner:1990:VVZ,% Bjorner:1990:VVZ,% Coenen:1995:HLV% }. \NAMECITE{verifiable}{% Hoare:1990:AAV% }. \NAMECITE{Verification}{% Broy:2011:SSS,% Hoare:2008:VFG,% Hoare:2021:PSI,% Hooman:1992:CVR,% Huisman:2000:JPV,% Manna:2010:TVE,% Poskitt:2012:HSV,% Woodcock:2021:VGC,% Cocco:1982:MEH,% Dasgupta:1984:UHL,% Fetzer:1988:PVV,% Hoare:2002:APV,% Hoare:2009:PSI,% Homeier:1995:MVV,% Lifschitz:1984:VPG,% Makowsky:1989:WSO,% Neuhold:1977:UHM,% Pritchard:1979:CPJ,% Shaner:2007:MVH,% Szczepanska:1991:HLV% }. \NAMECITE{verifications}{% Csirmaz:1981:PPV% }. \NAMECITE{Verified}{% Hoare:2008:VST,% Meyer:2008:VST,% Bicarregui:2006:VSR,% Hoare:2006:IVS,% Hoare:2009:VSI,% Homeier:1995:MVV,% Hoare:2021:VSI,% Mller:2021:FFY% }. \NAMECITE{verifier}{% Chlipala:2013:BSP% }. \NAMECITE{Verifying}{% Hartog:2002:VPP,% Hoare:2003:TVC,% Hoare:2003:VCGa,% Hoare:2004:TVC,% Reus:2001:HCV,% Ridge:2009:VDS,% Stoller:1995:VPU,% Wing:1989:VAD,% Bicarregui:2006:VSR,% Hoare:2003:VC,% Hoare:2003:VCGb,% Hoare:2005:VCG,% Sousa:2016:CHL% }. \NAMECITE{very}{% Fetzer:1988:PVV% }. \NAMECITE{via}{% Huisman:2000:JPV,% Rehof:2010:ADS% }. \NAMECITE{Viewpoint}{% Hoare:2009:VRA% }. \NAMECITE{viii}{% Anonymous:1987:BRC% }. \NAMECITE{Virtual}{% vonOheimb:2002:HLN% }. \NAMECITE{Vision}{% Hoare:2008:VST% }. \NAMECITE{Visions}{% Hoare:2004:VIF% }. \NAMECITE{VSTTE}{% Meyer:2008:VST% }. \NAMECITE{{{Vzaimode{{i}}}}}{% Khoar:1989:CVC% }. \NAMECITE{W}{% Barron:1975:BRS,% Barth:1974:BRJ,% Boyer:2002:MEW,% Feijen:1990:BOB,% Lloyd:1974:BRS% }. \NAMECITE{Was}{% Lewis:1997:BCI% }. \NAMECITE{Watered}{% Olsen:1997:LWJ% }. \NAMECITE{way}{% Hoare:1973:HLP% }. \NAMECITE{Weak}{% Makowsky:1989:WSO% }. \NAMECITE{Weakest}{% Hoare:1985:WP,% Hoare:1986:WPa,% Hoare:1986:WPb,% Hoare:1987:WP% }. \NAMECITE{Weakly}{% Hoofman:1991:WEM% }. \NAMECITE{WG}{% Meyer:2008:VST,% Hoare:1966:LWM% }. \NAMECITE{Which}{% Clarke:1979:PLC,% Bergstra:1982:SNS,% Page:1989:SME% }. \NAMECITE{while}{% Bergstra:1982:SNS,% Greif:1981:SSW,% Stirling:1988:GOG% }. \NAMECITE{while-programs}{% Bergstra:1982:SNS% }. \NAMECITE{{Whitehead}}{% Hoare:1979:CGW% }. \NAMECITE{Whither}{% Naumann:2019:WSP% }. \NAMECITE{widely}{% Boyer:1996:APO% }. \NAMECITE{{Wijngaarden}}{% Hoare:1968:LVW% }. \NAMECITE{{Windows}}{% Gozum:1997:LWC% }. \NAMECITE{Windsor}{% Bottaci:2010:TAI% }. \NAMECITE{Winner}{% Hoare:2016:PST% }. \NAMECITE{Without}{% Hoare:1996:HDS,% Olderog:1984:CPP% }. \NAMECITE{Work}{% Apt:2022:EWD,% Jones:2010:RWC% }. \NAMECITE{Works}{% Jones:2021:TPL% }. \NAMECITE{Workshop}{% Jones:2013:ICC% }. \NAMECITE{world}{% Tennent:1991:CPW% }. \NAMECITE{worth}{% Dijkstra:1999:FWT% }. \NAMECITE{Writings}{% Dijkstra:1982:SWC% }. \NAMECITE{Wybe}{% Apt:2022:EWD,% Hoare:2003:EWD% }. \NAMECITE{Ya}{% Baer:1965:RPP% }. \NAMECITE{Years}{% Apt:1981:TYH,% Hoare:2022:FYE,% McReynolds:1997:LBS,% Mller:2021:FFY,% Abdallah:2005:CSP,% Apt:1984:TYH,% Apt:2019:FYH,% Ashenhurst:1987:ATA% }. \NAMECITE{Yes}{% Hoare:2004:YWT% }. \NAMECITE{{Ynot}}{% Nanevski:2008:YDT% }. \NAMECITE{{Yu.}}{% Baer:1965:RPP% }. \NAMECITE{Z}{% Bjorner:1990:VVZ,% Morgan:1985:SSN,% Spivey:1989:ZNR% }. \NAMECITE{Zurich}{% Meyer:2008:VST% }.