% Safety-Critical Systems Bibliography
% October 1993
%
% Compiled by
%  Jonathan Bowen, Oxford University Computing Laboratory
% With contributions by
%  Victoria Stavridou, Royal Holloway College
%  Anders P. Ravn, Technical University of Denmark
%
% Minor corrections and additions by J.P. Bowen, November 1994
%

@string{prg = "Programming Research Group"}
@string{oucl = "Oxford University Computing Laboratory"}
@string{oxford = "11 Keble Road, Oxford OX1 3QD, UK"}
@string{uk = "UK"}
@string{LNCS = "Lecture Notes in Computer Science"}
@string{WICS = "Workshops in Computing"}
@string{Springer ="Springer-Verlag"}


@techreport{jpb:AECB,
  title = {Proposed Standard for Software for Computers in the
    Safety Systems of Nuclear Power Stations},
  month = {March},
  year = 1991,
  author = {D.L. Parnas},
  institution = {TRIO, Computing and Information Science,
    Queen's University},
  address = {Kingston, Ontario K7L 3N6, Canada},
  note = {
    Final Report for contract 2.117.1 for
    the Atomic Energy Control Board, Canada.
    Based on IEC Standard 880 \cite{jpb:IEC880}.}
}
% Communications Research Laboratory,
% Department of Electrical and Computer Engineering,
% McMaster University,
% Hamilton, Ontario L8S 4K1, Canada.

@techreport{jpb:VDM,
  author = {BSI},
  title = {{VDM} Specification Proto-Standard},
  note = {Draft},
  type = {BSI},
  number = {IST/5/50 document},
  institution = {British Standards Institute},
  month = {March},
  year = 1991
}

@techreport{jpb:MIL-STD-882B,
  author = {DoD},
  title = {Military Standard: System Safety Program Requirements},
  type = {Standard},
  number = {MIL-STD-882B},
  institution = {Department of Defense},
  address = {Washington DC 20301, USA},
  month = {30 March},
  year = 1984
}

@techreport{jpb:ESA91,
  author = {ESA},
  title = {{ESA} Software Engineering Standards},
  institution = {European Space Agency},
  address = {8--10 rue Mario-Nikis, 75738 Paris Cedex, France},
  type = {ESA},
  number = {PSS-05-0 Issue 2},
  month = {February},
  year = 1991
}

@book{jpb:EWICS88/89,
  editor = {Redmill, F.},
  title = {Dependability of Critical Computer Systems 1 \& 2},
  note = {European Workshop on Industrial Computer Systems
    Technical Committee 7 (EWICS TC7)},
  publisher = {Elsevier Applied Science},
  address = {London, UK},
  oter = {Crown House, Linton Road, Barking, Essex, IG11 8JU, UK},
  year = {1988/1989}
}

@techreport{jpb:FAA82,
  author = {FAA},
  title = {System Design Analysis},
  institution = {US Department of Transportation,
    Federal Aviation Administration},
  address = {Washington DC, USA},
  type = {Advisory Circular},
  number = {25.1309-2},
  month = {September},
  year = 1982
}

@book{jpb:PES1,
  title = {Programmable Electronic Systems in
    Safety Related Applications: 1.\ An Introductory Guide},
  author = {{Health and Safety Executive}},
  publisher = {HMSO},
  address = {Publications Centre, PO Box 276, London SW8 5DT, UK},
  year = 1987
}

@book{jpb:PES2,
  title = {Programmable Electronic Systems in
    Safety Related Applications: 2.\ General Technical Guidelines},
  author = {{Health and Safety Executive}},
  publisher = {HMSO},
  address = {Publications Centre, PO Box 276, London SW8 5DT, UK},
  year = 1987
}

@techreport{jpb:IEC880,
  author = {IEC},
  title = {Software for Computers in the Safety Systems of Nuclear
    Power Stations},
  institution = {International Electrotechnical Commission},
  type = {IEC},
  number = {880},
  year = 1986
}

@techreport{jpb:IEC65-WG9,
  author = {IEC},
  title = {Software for Computers in the Application of
    Industrial Safety Related Systems},
  institution = {International Electrotechnical Commission},
  note = {Technical Committee no.\ 65, Working Group 9 (WG9)},
  type = {IEC},
  number = {65A (Secretariat) 122, Version 1.0},
  month = {1 August},
  year = 1991
}
% Technical Committee no.\ 65,
% Working Group 9,
% 1989. (BS89/33006DC)

@techreport{jpb:IEC65-WG10,
  author = {IEC},
  title = {Functional Safety of Programmable Electronic Systems:
    Generic Aspects},
  institution = {International Electrotechnical Commission},
  note = {Technical Committee no.\ 65, Working Group 10 (WG10)},
  type = {IEC},
  number = {65A (Secretariat) 123},
  month = {February},
  year = 1992
}
% Technical Committee no.\ 65,
% Working Group 10,
% 1989. (BS89/33005DC)

@techreport{jpb:IEEE91,
  author = {IEEE},
  title = {Standard for Software Safety Plans},
  note = {Preliminary -- subject to revision},
  type = {Draft standard},
  number = {P1228},
  institution = {
    Software Safety Plans Working Group,
    Software Engineering Standards Subcommittee,
    IEEE Computer Society},
  address = {USA},
  month = {July},
  year = 1991
}

@techreport{jpb:ISO87,
  author = {ISO},
  title = {{JTC1} Statement of Policy on
    Formal Description Techniques},
  type = {ISO/IEC},
  number = {JTC1 N145 and ISO/IEC JTC1/SC18 N13333},
  institution = {International Standards Organization},
  address = {Geneva, Switzerland},
  year = 1987
}

@techreport{jpb:LOTOS,
  author = {ISO},
  title = {{ISO} 8807: Information Processing Systems -- Open Systems
    Interconnection -- {LOTOS} -- A Formal Description Technique Based
    on the Temporal Ordering of Observational Behaviour},
  type = {Standard},
  note = {First edition},
  institution = {International Standards Organization},
  address = {Geneva, Switzerland},
  month = {15 February},
  year = 1987
}

@techreport{jpb:00-55,
  author = {MoD},
  title = {The Procurement of Safety Critical Software in Defence
    Equipment (Part 1: Requirements, Part 2: Guidance)},
  type = {Interim Defence Standard},
  number = {00-55, Issue 1},
  institution = {Ministry of Defence, Directorate of Standardization},
  address = {Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK},
  month = {5 April},
  year = 1991
}

@techreport{jpb:00-56,
  author = {MoD},
  title = {Hazard Analysis and Safety Classification of the Computer and
    Prog\-rammable Electronic System Elements of Defence Equipment},
  type = {Interim Defence Standard},
  number = {00-56, Issue 1},
  institution = {Ministry of Defence, Directorate of Standardization},
  address = {Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK},
  month = {5 April},
  year = 1991
}

@techreport{jpb:OH90,
  author = {{Ontario Hydro}},
  title = {Standard for Software Engineering of Safety Critical
    Software},
  type = {Ref.},
  number = {982~C-H~69002-0001},
  institution = {Ontario Hydro},
  address = {700 University Avenue, Toronto, Ontario M5G 1X6, Canada},
  month = {21 December},
  year = 1990
}

@techreport{jpb:RIA91,
  author = {RIA},
  title = {Safety Related Software for Railway Signalling},
  type = {BRB/LU Ltd/RIA technical specification no.},
  number = 23,
  note = {Consultative Document},
  institution = {Railway Industry Association},
  address = {6 Buckingham Gate, London SW1E 6JP, UK},
  year = 1991
}

@techreport{jpb:DO-178A,
  author = {RTCA},
  title = {Software Considerations in Airborne Systems and Equipment
    Certification},
  type = {Guideline},
  number = {DO-178A},
  institution = {Radio Technical Commission for Aeronautics},
  address = {One McPherson Square, 1425 K Street N.W., Suite 500,
    Washington DC 20005, USA},
  month = {March},
  year = 1985
}

@techreport{jpb:DO-185,
  author = {RTCA},
  title = {Minimum Operational Performance Standards for Traffic
    Alert and Collision Avoidance System (TCAS) Airborne Equipment
    -- Consolidated Edition},
  type = {Guideline},
  number = {DO-185},
  institution = {Radio Technical Commission for Aeronautics},
  address = {One McPherson Square, 1425 K Street N.W., Suite 500,
    Washington DC 20005, USA},
  month = {6 September},
  year = 1990
}

@book{jpb:SafeIT1,
  editor = {Bloomfield, R.E.},
  title = {{SafeIT1} -- The Safety of Programmable Electronic Systems},
  note = {Safety-Related Working Group (SRS-WG),
    Interdepartmental Committee on Software Engineering (ICSE)},
  publisher = {Department of Trade and Industry},
  address = {ITD7a -- Room 840, Kingsgate House,
    66--74 Victoria Street, London SW1E 6SW, UK},
  month = {June},
  year = 1990
}
% A government consultation document on activities to promote the
% safety of computer controlled systems.

@book{jpb:SafeIT2,
  editor = {Bloomfield, R.E. and Brazendale, J.},
  title = {{SafeIT2} -- A Framework for Safety Standards},
  note = {Safety-Related Working Group (SRS-WG),
    Interdepartmental Committee on Software Engineering (ICSE)},
  publisher = {Department of Trade and Industry},
  address = {ITD7a -- Room 840, Kingsgate House,
    66--74 Victoria Street, London SW1E 6SW, UK},
  month = {June},
  year = 1990
}

%% Incomplete ref.
@techreport{jpb:UN64,
  author = {{United Nations}},
  title = {{UN} Committee for the Transport of Dangerous Goods},
  institution = {United Nations},
  type = {Technical Report},
  year = 1964
}

@techreport{jpb:Zstandard,
  author = {S.M. Brien and J.E. Nicholls},
  title = {{Z} Base Standard},
  institution = {Oxford University Computing Laboratory},
  address = {11 Keble Road, Oxford OX1 3QD, UK},
  type = {Technical Monograph},
  number = {PRG-107},
  other = {ZIP/PRG/92/121, SRC Document: 132, Version 1.0},
  ISBN = {0-902928-84-8},
  month = {November},
  year = {1992},
  note = {Accepted for ISO standardization, ISO/IEC JTC1/SC22.}
}

@manual{jpb:Abrial91,
  author = {Abrial, J.R.},
  title = {The {B} reference manual},
  organization = {Edinburgh Portable Compilers},
  address = {17 Alva Street, Edinburgh EH2 4PH, UK},
  year = 1991
}

@inproceedings{jpb:ALNSS91,
  author = {Abrial, J.R. and Lee, M.K.O. and Neilson, D.S. and
    Scharbach, P.N. and S\o{}rensen, I.H.},
  title = {The {B}-method},
  editor = {Prehn, S. and Toetenel, W.J.},
  booktitle = {VDM'91: Formal Software Development Methods,
    Volume 2},
  publisher = {Springer-Verlag},
  series = LNCS,
  year = 1991,
  volume = 552,
  pages = {398-405}
}

@article{jpb:AC92,
  author = {Anderson, S. and Cleland, G.},
  title = {Adopting mathematically-based methods for safety-critical
    systems production},
  editor = {Redmill, F.},
  journal = {Safety Systems:
    The Safety-Critical Systems Club Newsletter},
  institution = {Centre for Software Reliability},
  address = {University of Newcastle upon Tyne, Newcastle NE1 7RU, UK},
  month = {January},
  year = 1992,
  volume = 1,
  number = 2,
  pages = 6
}

@inproceedings{jpb:Archinoff90,
  author = {Archinoff, G.H. and Hohendorf, R.J. and Wassyng, A.
    and Quigley, B. and Borsch, M.R.},
  title = {Verification of the shutdown system software
    at the {Darlington} nuclear generating station},
  booktitle = {International Conference on Control and
    Instrumentation in Nuclear Installations},
  organization = {The Institution of Nuclear Engineers},
  address = {Glasgow, UK},
  month = {May},
  year = 1990
}

@incollection{jpb:Augarten84,
  author = {Augarten, S.},
  title = {The {Whirlwind} project},
  booktitle = {Bit by Bit: An Illustrated History of Computers},
  chapter = 7,
  publisher = {Ticknor \& Fields},
  address = {New York, USA},
  year = 1984,
  pages = {195-223}
}

@misc{jpb:Babel87,
  author = {Babel, P.S.},
  title = {Software integrity program},
  howpublished = {Aeronautical Systems Division, U.S.\ Airforce},
  month = {April},
  year = 1987
}

@article{jpb:BM92,
  author = {Barroca, L. and McDermid, J.A.},
  title = {Formal methods: Use and relevance for the development
    of safety critical systems},
  journal = {The Computer Journal},
  volume = 35,
  number = 6,
  pages = {579-599},
  month = {December},
  year = 1992
}

@inproceedings{jpb:BSC91,
  author = {Barden, R. and Stepney, S. and Cooper, D.},
  title = {The use of {Z}},
  editor = {Nicholls, J.E.},
  booktitle = {Z User Workshop, York 1991},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  year = 1992,
  pages = {99-124}
}

%% Check next reference with the published proceedings
@inproceedings{jpb:Barnes89,
  author = {Barnes, M.},
  title = {Dependable computing in the {UK}},
  booktitle = {Can we rely on computers?
    International Working Conference on
    Dependable Computing for Critical Applications},
  note = {IFIP Working Group 10.4 on
    Dependable Computing and Fault Tolerance},
  month = {August},
  year = 1989,
  pages = {7-14}
}

@inproceedings{jpb:HPSL,
  author = {Bear, S.},
  title = {An overview of {HP-SL}},
  editor = {Prehn, S. and Toetenel, W.J.},
  booktitle = {VDM'91: Formal Software Development Methods, Volume 1},
  publisher = {Springer-Verlag},
  series = LNCS,
  year = 1991,
  volume = 551,
  pages = {571-587}
}

@incollection{jpb:Bennett91,
  author = {Bennett, P.A.},
  title = {Safety},
  editor = {McDermid, J.A.},
  booktitle = {Software Engineer's Reference Book},
  chapter = 60,
  publisher = {Butterworth-Heinemann Ltd.},
  address = {Oxford, UK},
  year = 1991
}

@article{jpb:Bjorner89,
  author = {D. Bj\o{}rner and C.A.R.\ Hoare and J.P. Bowen and
    {He Jifeng} and H. Langmaack and E.-R. Olderog and U. Martin and
    V. Stavridou and F. Nielson and H.R. Nielson and H. Barringer and
    D. Edwards and H.H. L\o{}vengreen and A.P. Ravn and H. Rischel},
  title = {A {ProCoS} Project Description: {ESPRIT BRA} 3104},
  journal = {Bulletin of the European Association for Theoretical
    Computer Science (EATCS)},
  ISSN = {0252-9742},
  year = 1989,
  volume = 39,
  pages = {60-73}
}

@article{jpb:BF86,
  author = {R.E. Bloomfield and P.K.D. Froome},
  title = {The application of formal methods to the assessment of high
    integrity software},
  journal = {IEEE Transactions on Software Engineering},
  month = {September},
  year = 1986,
  volume = 12,
  number = {9},
  pages = {988-993}
}

@article{jpb:BFM89,
  author = {Bloomfield, R.E. and Froome, P.K.D. and Monahan, B.Q.},
  title = {Formal methods in the production and assessment of
    safety critical software},
  journal = {Reliability Engineering \& System Safety},
  volume = 32,
  number = 1,
  year = 1989,
  pages = {51-66},
  note = {Also in \cite{jpb:LM91}}
}

@article{jpb:BBRT90,
  author = {Blyth, D. and Boldyreff, C. and
    Ruggles, C. and Tetteh-Lartey, N.},
  title = {The case for formal methods in standards},
  journal = {IEEE Software},
  month = {September},
  year = 1990,
  pages = {65-67}
}

@article{jpb:Boebert80,
  author = {Boebert, W.E.},
  title = {Formal verification of embedded software},
  journal = {ACM SIGSOFT Software Engineering Notes},
  month = {July},
  year = 1980,
  volume = 5,
  number = 3,
  pages = {41-42}
}

%% Incomplete ref.
@misc{jpb:Boehm88,
  author = {Boehm, B.},
  title = {Software risk management tutorial},
  howpublished = {TRW-ACM Seminar},
  month = {April},
  year = 1988
}

@inproceedings{jpb:BB92a,
  author = {Breuer, P.T. and Bowen, J.P.},
  title = {Decompilation {\em is} the Efficient Enumeration of Types},
  editor = {Billaud, M. and others},
  booktitle = {Journ\'ees de Travail WSA'92 Analyse Statique},
  volume = {BIGRE 81--82},
  organization = {IRISA-Campus de Beaulieu},
  address = {F-35042 Rennes cedex, France},
  year = 1992,
  pages = {255-273}
}

@incollection{jpb:BB92,
  author = {Bowen, J.P. and Breuer, P.T.},
  title = {Decompilation},
  editor = {{van Zuylen}, H.},
  booktitle = {The REDO Compendium:
    Reverse Engineering for Software Maintenance},
  chapter = 10,
  pages = {131-138},
  publisher = {John Wiley \& Sons},
  year = 1993
}

@inproceedings{jpb:BS92,
  author = {Bowen, J.P. and Stavridou, V.},
  title = {Formal methods and software safety},
  editor = {Frey, H.H.},
  booktitle = {Safety of computer control systems 1992 ({SAFECOMP'92}),
    Computer Systems in Safety-critical Applications,
    Proc.\ IFAC Symposium},
  location {Z\"urich, Switzerland, 28--30 October 1992},
  publisher = {Pergamon Press},
  year = 1992,
  pages = {93-98}
}

@inproceedings{jpb:BS93,
  author = {Bowen, J.P. and Stavridou, V.},
  title = {The industrial take-up of formal methods in
    safety-critical and other areas: A perspective},
  editor = {Woodcock, J.C.P. and Larsen, P.G.},
  booktitle = {FME'93: Industrial-Strength Formal Methods},
  location = {Odense, Denmark, 19--23 April 1993},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 670,
  pages = {183-195},
  year = 1993,
}

@book{jpb:BM79,
  author = {Boyer, R.S. and Moore, J.S.},
  title = {A Computational Logic},
  publisher = {Academic Press},
  series = {ACM Monograph Series},
  address = {New York, USA},
  year = 1979
}

@book{jpb:BM88,
  author = {Boyer, R.S. and Moore, J.S.},
  title = {A Computational Logic Handbook},
  publisher = {Academic Press},
  address = {Boston, USA},
  year = 1988
}

@techreport{jpb:BH90,
  author = {Brock, B. and Hunt, W.A.},
  title = {Report on the formal specification
    and partial verification of the {VIPER} microprocessor},
  type = {Technical Report},
  number = {46},
  institution = {Computational Logic Inc.},
  address = {Austin, Texas, USA},
  month = {January},
  year = 1990
}

@inproceedings{jpb:Brown90,
  author = {Brown, M.J.D.},
  title = {Rationale for the development of the UK defence
    standards for safety-critical computer software},
  booktitle = {Proc.\ COMPASS'90, Washington DC, USA},
  month = {June},
  year = 1990
}

@article{jpb:Burns91,
  author = {Burns, A.},
  title = {The HCI component of dependable real-time systems},
  journal = {IEE/BCS Software Engineering Journal},
  month = {July},
  year = 1991,
  volume = 6,
  number = 4,
  pages = {168-174}
}

@article{jpb:Butler93,
  author = {Butler, R.W. and Finelli, G.B.},
  title = {The infeasibility of experimental quantification of
    life-critical software reliability},
  journal = {IEEE Transactions on Software Engineering},
  volume = 19,
  number = 1,
  pages = {3-12},
  month = {January},
  year = 1993
}

@article{jpb:BM91,
  author = {Buxton, J.N. and Malcolm, R.},
  title = {Software technology transfer},
  journal = {IEE/BCS Software Engineering Journal},
  month = {January},
  year = 1991,
  volume = 6,
  number = 1,
  pages = {17-23}
}

@unpublished{jpb:Canning91,
  author = {Canning, A.},
  title = {Assessment at the requirements stage of a project},
  month = {October},
  year = 1991,
  note = {Presented at 2nd Safety Critical Systems Club Meeting,
    Beaconsfield, UK, October 1991.
    Available from Advanced Software Department,
    ERA Technology Ltd, Cleeve Rd, Leatherhead KT22 7SA, UK.}
}

@inproceedings{jpb:Chapront92,
  author = {Chapront, P.},
  title = {Vital coded processor and safety related software design},
  pages = {141-145},
  editor = {Frey, H.H.},
  booktitle = {Safety of computer control systems 1992 ({SAFECOMP'92}),
    Computer Systems in Safety-critical Applications,
    Proc.\ IFAC Symposium}.
  location {Z\"urich, Switzerland, 28--30 October 1992},
  publisher = {Pergamon Press},
  year = 1992
}

@book{jpb:Char90,
  author = {Charette, R.N.},
  title = {Applications Strategies for Risk Analysis},
  publisher = {McGraw Hill},
  series = {Software Engineering Series},
  year = 1990
}

@article{jpb:CC88,
  author = {Clutterbuck, D.L. and Carr\'e, B.A.},
  title = {The verification of low-level code},
  journal = {IEE/BCS Software Engineering Journal},
  month = {May},
  year = 1988,
  volume = 3,
  number = 3,
  pages = {97-111}
}

@incollection{jpb:CP90,
  author = {Cohen, B. and Pitt, D.H.},
  title = {The identification and discharge of proof obligations},
  booktitle = {Testing Large Software Systems},
  publisher = {Wolverhampton Polytechnic},
  address = {UK},
  other = {Bernie Cohen is at Dept.\ of Computer Science,
    City University, London, UK.},
  year = 1990
}

@incollection{jpb:Cohn88a,
  author = {Cohn, A.J.},
  title = {A proof of correctness of the {Viper} microprocessor:
    the first level},
  editor = {Birtwistle, G. and Subramanyam, P.A.},
  booktitle = {VLSI Specification, Verification and Synthesis},
  publisher = {Kluwer Academic Publishers},
  year = 1988
}

@inproceedings{jpb:Cohn88b,
  author = {Cohn, A.J.},
  title = {Correctness properties of the {Viper} block model:
    the second level},
  booktitle = {Proc.\ 2nd Banff Workshop on Hardware Verification},
  publisher = {Springer-Verlag},
  year = 1988
}

@article{jpb:Cohn89,
  author = {Cohn, A.J.},
  title = {The notion of proof in hardware verification},
  journal = {Journal of Automated Reasoning},
  month = {May},
  year = 1989,
  volume = 5,
  pages = {127-139}
}

@inproceedings{jpb:Coleman90,
  author = {Coleman, D.},
  title = {The technology transfer of formal methods:
    what's going wrong?},
  booktitle = {Proc.\ 12th ICSE Workshop on
    Industrial Use of Formal Methods, Nice, France},
  month = {March},
  year = 1990
}

@book{jpb:Craig91,
  author = {Craig, I.},
  title = {The Formal Specification of Advanced {AI} Architectures},
  publisher = {Ellis Horwood},
  series = {AI Series},
  year = 1991
}

@book{jpb:Craigen90,
  editor = {Craigen, D.},
  title = {Formal Methods for Trustworthy Computer Systems ({FM89})},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  year = 1990
}

@article{jpb:Cullyer85,
  author = {Cullyer, W.J.},
  title = {Hardware integrity},
  journal = {Aeronautical Journal of the Royal Aeronautical Society},
  month = {September},
  year = 1985,
  pages = {263-268}
}

@inproceedings{jpb:Cullyer88,
  author = {Cullyer, W.J.},
  title = {High integrity computing},
  editor = {Joseph, M.},
  booktitle = {Formal Techniques in Real-Time and
    Fault-Tolerant Systems},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 331,
  pages = {1-35},
  year = 1988
}

@article{jpb:CP87,
  author = {Cullyer, W.J. and Pygott, C.H.},
  title = {Application of formal methods to the {VIPER} microprocessor},
  journal = {IEE Proceedings, Part E,
    Computers and Digital Techniques},
  month = {May},
  year = 1987,
  volume = 134,
  number = 3,
  pages = {133-141}
}

@techreport{jpb:Curzon92,
  author = {Curzon, P.},
  title = {Of what use is a verified compiler specification?},
  type = {Technical Report},
  number = 274,
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  month = {November},
  year = 1992
}

@article{jpb:CBH91,
  author = {Cyrus, J.L. and Bledsoe, J.D. and Harry, P.D.},
  title = {Formal specification and structured design in
    software development},
  journal = {Hewlett-Packard Journal},
  month = {December},
  year = 1991,
  pages = {51-58}
}

@techreport{jpb:Davies91,
  author = {Davies, J.},
  title = {Specification and proof in real-time systems},
  type = {Technical Monograph},
  number = {PRG-93},
  institution = {Programming Research Group,
    Oxford University Computing Laboratory},
  address = {UK},
  month = {April},
  year = 1991
}

@article{jpb:deCham91,
  author = {{de Champeaux}, D. and others},
  title = {Formal techniques for {OO} software development},
  booktitle = {OOPSLA'91 Conference in
    Object-Oriented Programming Systems, Languages, and Applications},
  journal = {ACM SIGPLAN Notices},
  publisher = {ACM Press},
  month = {November},
  year = 1991,
  volume = 26,
  number = 11,
  pages = {166-170}
}

@book{jpb:DTI:survey,
  author = {{Coopers \& Lybrand}},
  title = {Safety related computer controlled systems market study},
  note = {Review for the Department of Trade and Industry},
  publisher = {HMSO},
  address = {London, UK},
  year = 1992
}

@book{jpb:Dix91,
  author = {Dix, A.},
  title = {Formal methods for interactive systems},
  publisher = {Academic Press},
  year = 1991,
  ISBN = {0-12-218315-0}
}

@book{jpb:Dyer92,
  author = {Dyer, M.},
  title = {The {Cleanroom} Approach to Quality Software Development},
  publisher = {John Wiley \& Sons},
  series = {Series in Software Engineering Practice},
  year = 1992
}

@techreport{jpb:FFFH89,
  author = {Finn, S. and Fourman, M. and Francis, M. and Harris, R.},
  title = {Formal system design -- interactive synthesis based on
    computer-assisted formal reasoning},
  type = {Technical Report},
  institution = {Abstract Hardware Ltd.},
  address = {Edinburgh, UK},
  other = {Superseded by \cite{jmjh:Finn}.}
  year = 1989
}

@inproceedings{jpb:FL91,
  author = {Fenton, N. and Littlewood, B.},
  title = {Evaluating software engineering standards and methods},
  booktitle = {Proc.\ 2\`emes Rencontres Qualite\'e Logiciel \&
    Eurometrics '91},
  month = {March},
  year = 1991,
  pages = {333-340}
}

@proceedings{jpb:Frey92,
  editor = {Frey, H.H.},
  booktitle = {Safety of computer control systems 1992 ({SAFECOMP'92}),
    Computer Systems in Safety-critical Applications,
    Proc.\ IFAC Symposium},
  location {Z\"urich, Switzerland, 28--30 October 1992},
  publisher = {Pergamon Press},
  year = 1992
}

@article{jpb:Glass80,
  author = {Glass, R.L.},
  title = {Software vs.\ hardware errors},
  journal = {IEEE Computer},
  month = {December},
  year = 1980,
  volume = 23,
  number = 12
}

@techreport{jpb:OBJ3,
  author = {Goguen, J. and Winkler, T.},
  title = {Introducing {OBJ3}},
  type = {Technical Report},
  number = {SRI-CSL-88-9},
  institution = {SRI International},
  address = {Menlo Park, California, USA},
  month = {August},
  year = 1988
}

@article{jpb:GF91,
  author = {Goldsack, S.J. and Finkelstein, A.C.W.},
  title = {Requirements engineering for real-time systems},
  journal = {IEE/BCS Software Engineering Journal},
  month = {May},
  year = 1991,
  volume = 6,
  number = 3,
  pages = {101-115}
}

@inproceedings{jpb:GY91,
  author = {Good, D.I. and Young, W.D.},
  title = {Mathematical methods for digital system development},
  editor = {Prehn, S. and Toetenel, W.J.},
  booktitle = {VDM'91: Formal Software Development Methods,
    Volume 2},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 552,
  pages = {406-430},
  year = 1991
}


@incollection{jpb:HOL,
  author = {Gordon, M.J.C.},
  title = {{HOL}: A proof generating system for {Higher-Order Logic}},
  editor = {Birtwistle, G. and Subramanyam, P.A.},
  booktitle = {VLSI Specification, Verification and Synthesis},
  publisher = {Kluwer Academic Publishers},
  year = 1988,
  pages = {73-128}
}

@unpublished{jpb:Gordon91b,
  author = {Gordon, M.J.C.},
  title = {Hard real-time programming},
  note = {Draft, University of Cambridge, Computer Laboratory, UK},
  year = 1991
}

@incollection{jpb:Gries90,
  author = {Gries, D.},
  title = {Influences (or lack thereof) of formalism
    in teaching programming and software engineering},
  editor = {Dijkstra, E.W.},
  booktitle = {Formal Development of Programs and Proofs},
  chapter = 18,
  publisher = {Addison Wesley},
  series = {University of Texas at Austin Year of Programming Series},
  year = 1990,
  pages = {229-236}
}

@inproceedings{jpb:GH90,
  author = {Guiho, G. and Hennebert, C.},
  title = {{SACEM} software validation},
  booktitle = {Proc.\ 12th International Conference on
    Software Engineering (ICSE)},
  publisher = {IEEE Computer Society Press},
  month = {March},
  year = 1990,
  pages = {186-191}
}

@article{jpb:HK92,
  author = {Halang, W.A. and Kr\"amer, B.},
  title = {Achieving high integrity of process control software by
    graphical design and formal verification},
  journal = {IEE/BCS Software Engineering Journal},
  month = {January},
  year = 1992,
  volume = 7,
  number = 1,
  pages = {53-64}
}

@article{jpb:Hall90,
  author = {Hall, J.A.},
  title = {Seven myths of formal methods},
  journal = {IEEE Software},
  month = {September},
  year = 1990,
  pages = {11-19}
}

@article{jpb:Hall89,
  author = {Hall, P.A.V.},
  title = {Software development standards},
  journal = {IEE/BCS Software Engineering Journal},
  month = {May},
  year = 1989,
  volume = 4,
  number = 3,
  pages = {143-147}
}

@book{jpb:Hammer72,
  author = {Hammer, W.},
  title = {Handbook of System and Product Safety},
  publisher = {Prentice-Hall},
  address = {Englewood Cliffs, New Jersey, USA},
  year = 1972
}

@inproceedings{jpb:Harrison91,
  author = {Harrison, M.D.},
  title = {Engineering human error tolerant software},
  editor = {Nicholls, J.E.},
  booktitle = {Z User Workshop, York 1991},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  year = 1992,
  pages = {191-204}
}

@book{jpb:HT90,
  editor = {Harrison, M.D. and Thimbleby, H.},
  title = {Formal methods in HCI},
  publisher = {Cambridge University Press},
  address = {UK},
  year = 1990
}

@article{jpb:Helps86,
  author = {Helps, K.A.},
  title = {Some verification tools and methods for airborne
    safety-critical software},
  journal = {IEE/BCS Software Engineering Journal},
  month = {November},
  year = 1986,
  volume = 1,
  number = 6,
  pages = {248-253}
}

@inproceedings{jpb:Hill88,
  author = {Hill, J.V.},
  title = {The development of high reliability software --
    {RR\&A}'s experience for safety critical systems},
  booktitle = {Second IEE/BCS Conference, Software Engineering 88},
  note = {Conference Publication No.\ 290},
  month = {July},
  year = 1988,
  pages = {169-172}
}

@incollection{jpb:Hill91,
  author = {Hill, J.V.},
  title = {Software development methods in practice},
  booktitle = {Microprocessor Based Protection Systems},
  publisher = {Elsevier},
  other = {Presented at 6th Annual Conference on Computer Assurance
    (COMPASS), 1991},
  year = 1991
}

@article{jpb:Hoare91a,
  author = {Hoare, C.A.R.},
  title = {The Transputer and Occam: A personal story},
  journal = {Concurrency: Practice and Experience},
  month = {August},
  year = 1991,
  volume = 3,
  number = 4,
  pages = {249-264}
}

@incollection{jpb:Hoare91,
  author = {Hoare, C.A.R.},
  title = {Algebra and models},
  editor = {Bj\o{}rner, D. and Langmaack, H. and Hoare, C.A.R.},
  booktitle = {ProCoS I Final Deliverable},
  month = {January},
  year = 1993,
  publisher = {Department of Computer Science,
    Technical University of Denmark},
  address = {Lyngby, Denmark},
  note = {ProCoS Technical Report [ID/DTH DB 13/1]}
}

@book{jpb:HG92,
  editor = {Hoare, C.A.R. and Gordon, M.J.C.},
  title = {Mechanized Reasoning and Hardware Design},
  publisher = {Prentice Hall
    International Series in Computer Science},
  year = 1992
}

@inproceedings{jpb:HG92b,
  author = {Hoare, C.A.R. and Gordon, M.J.C. and others},
  title = {Mechanized Reasoning and Hardware Design},
  booktitle = {Philosophical Transactions of the Royal Society
    of London},
  series = {Series A},
  location = {Royal Society, London, UK, 3--4 October 1991},
  publisher = {Royal Society},
  address = {London, UK},
  volume = 339,
  pages = {1-151},
  year = 1992
}

@inproceedings{jpb:HHBP90,
  author = {C.A.R. Hoare and {He Jifeng} and J.P. Bowen
    and P.K. Pandya},
  title = {An Algebraic Approach to Verifiable
    Compiling Specification and Prototyping
    of the {ProCoS} Level 0 Programming Language},
  booktitle = {ESPRIT '90 Conference Proceedings},
  other = {Edited by Directorate-General XIII of the CEC},
  location = {Brussels, Belgium, 12--15 November 1990},
  publisher = {Kluwer Academic Publishers},
  pages = {804-818},
  year = {1990}
}

@inproceedings{jpb:HK91,
  author = {Houston, I. and King, S.},
  title = {{CICS} project report: Experiences and results
    from the use of {Z} in {IBM}},
  editor = {Prehn, S. and Toetenel, W.J.},
  booktitle = {VDM'91: Formal Software Development Methods, Volume 1},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 551,
  pages = {588-603},
  year = 1991
}

@inproceedings{jpb:Humphrey89,
  author = {Humphrey, W.S. and Kitson, D.H. and Casse, T.C.},
  title = {The state of software engineering practice:
    a preliminary report},
  booktitle = {Proc.\ 11th International Conference on
    Software Engineering (ICSE), Pittsburgh, USA},
  month = {May},
  year = 1989,
  pages = {277-288}
}

@misc{jpb:IEE92,
  key = {Institution of Electrical Engineers},
  title = {Safety-related systems:
    A professional brief for the engineer},
  howpublished = {The Institution of Electrical Engineers (IEE),
    Savoy Place, London WB2R 0BR, UK},
  month = {January},
  year = 1992
}

@incollection{jpb:Ince88,
  author = {Ince, D.},
  title = {Ultra-reliable software and the mail order programmer},
  booktitle = {Software Development: Fashioning the baroque},
  chapter  = 10,
  publisher = {Oxford University Press, Oxford Science Publications},
  year = 1988,
  pages = {93-97}
}

@article{jpb:Iyer85,
  author = {Iyer, R.K. and Verlardi, P.},
  title = {Hardware-related software errors: Measurement and analysis},
  journal = {IEEE Transactions on Software Engineering},
  volume = 11,
  number = 2,
  month = {February},
  year = 1985
}
% Pages?

@article{jpb:Jacky89,
  author = {Jacky, J.},
  title = {Programmed for disaster:
    Software errors that imperil lives},
  journal = {The Sciences},
  month = {September/October},
  year = 1989,
  pages = {22-27}
}

@article{jpb:Jacky90,
  author = {Jacky, J.},
  title = {Formal specifications for a clinical cyclotron
    control system},
  editor = {Moriconi, M.},
  booktitle = {Proc.\ ACM SIGSOFT International Workshop on
    Formal Methods in Software Development},
  journal = {ACM SIGSOFT Software Engineering Notes},
  publisher = {ACM Press},
  month = {September},
  year = 1990,
  volume = 15,
  number = 4,
  pages = {45-54}
}

@incollection{jpb:Jacky91a,
  author = {Jacky, J.},
  title = {Safety-critical computing:
    Hazards, practices, standards and regulation},
  editor = {Dunlop, C. and Kling, R.},
  booktitle = {Computerization and controversy},
  chapter = 5,
  publisher = {Academic Press},
  year = 1991,
  pages = {612-631}
}

@techreport{jpb:Jacky91b,
  author = {Jacky, J.},
  title = {Verification, analysis and synthesis of safety interlocks},
  type = {Technical Report},
  number = {91-04-01},
  institution = {Department of Radiation Oncology RC-08,
    University of Washington},
  address = {Seattle, WA 98195, USA},
  month = {April},
  year = 1991
}

@article{jpb:JLHM91,
  author = {Jaffe, M.S. and Leveson, N.G. and
    Heimdahl, M.P. and Melhart, B.E.},
  title = {Software requirements analysis for real-time
    process-control systems},
  journal = {IEEE Transactions on Software Engineering},
  volume = 17,
  number = 3,
  pages = {241-258},
  month = {March},
  year = 1991
}

@misc{jpb:JHTIC91,
  author = {Joannou, P.K. and Harauz, J. and Tremaine, D.R. and
    Ichiyen, N. and Clark, A.B.},
  title = {The {Canadian} nuclear industry's initiative in real-time
    software engineering},
  howpublished = {Ontario Hydro,
    700 University Avenue, Toronto, Ontario M5G 1X6, Canada},
  year = 1991
}

@book{jpb:Jones90,
  author = {Jones, C.B.},
  title = {Systematic Software Development using {VDM}},
  edition = {2nd},
  publisher = {Prentice Hall
    International Series in Computer Science},
  year = 1990
}

@book{jpb:Kandel88,
  author = {Kandel, A. and Avni, E.},
  title = {Engineering Risk and Hazard Assessment},
  volume = {I},
  publisher = {CRC Press},
  address = {Boca Raton, Florida, USA},
  year = 1988
}

@article{jpb:KL90,
  author = {Knight, J.C. and Leveson, N.G.},
  title = {A reply to the criticisms of the
    {Knight} \& {Leveson} experiment},
  journal = {ACM SIGSOFT Software Engineering Notes},
  month = {January},
  year = 1990,
  volume = 15,
  number = 1,
  pages = {25-35}
}

@inproceedings{jpb:KK93,
  author = {Knight, J.C. and Kienzle, D.M.},
  title = {Preliminary experience using {Z} to specify
    a safety-critical system},
  editor = {Bowen, J.P. and Nicholls, J.E.},
  booktitle = {Z User Workshop, London 1992},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {109-118},
  year = 1993
}

@article{jpb:KZFKP91,
  author = {Kopetz, H. and Zainlinger, R. and Fohler, G. and
    Kantz, H. and Puschner, P.},
  title = {The design of real-time systems:
    From specification to implementation and verification},
  journal = {IEE/BCS Software Engineering Journal},
  month = {May},
  year = 1991,
  volume = 6,
  number = 3,
  pages = {73-82}
}

@article{jpb:LF91,
  author = {Ladeau, B.R. and Freeman, C.},
  title = {Using formal specification for product development},
  journal = {Hewlett-Packard Journal},
  month = {December},
  year = 1991,
  pages = {62-66}
}

@inproceedings{jpb:Laprie85,
  author = {Laprie, J.C.},
  title = {Dependable computing and fault tolerance: Concepts and
    terminology},
  booktitle = {Proc.\ 15th IEEE Int.\ Symp.\ on Fault Tolerant
    Computing, Ann Arbor, Michigan, USA},
  year = 1985
}

@incollection{jpb:Laprie89,
  author = {Laprie, J.C.},
  title = {Dependability:
    A unifying concept for reliable computing and fault tolerance},
  editor = {Anderson, T.},
  booktitle = {Dependability of Resilient Computers},
  chapter = 1,
  publisher = {Blackwell Scientific Publications},
  address = {Oxford, UK},
  year = 1989,
  pages = {1-28}
}

@book{jpb:Laprie91,
  editor = {Laprie, J.C.},
  title = {Dependability: Basic Concepts and Terminology},
  publisher = {Springer-Verlag},
  year = 1991
}

@article{jpb:Leveson86,
  author = {Leveson, N.G.},
  title = {Software safety: Why, what and how},
  journal = {ACM Computing Surveys},
  month = {June},
  year = 1986,
  volume = 18,
  number = 2,
  pages = {125-163}
}

@article{jpb:Leveson91,
  author = {Leveson, N.G.},
  title = {Software safety in embedded computer systems},
  journal = {Communications of the ACM},
  month = {February},
  year = 1991,
  volume = 34,
  number = 2,
  pages = {34-46}
}

@techreport{jpb:LT92,
  author = {Leveson, N.G. and Turner, C.T.},
  title = {An investigation of the {Therac-25} accidents},
  type = {UCI Technical Report},
  number = {92-108},
  note = {Also University of Washington Technical Report 92-11-05},
  institution = {Information and Computer Science Dept.,
    University of California},
  address = {Irvine, CA 92717, USA},
  year = 1992
  other = {Published as \cite{jpb:LT93}.}
}

@article{jpb:LT93,
  author = {Leveson, N.G. and Turner, C.T.},
  title = {An Investigation of the {Therac-25} Accidents},
  journal = {IEEE Computer},
  volume = 26,
  number = 7,
  pages = {18-41},
  month = {July},
  year = 1993
}

@article{jpb:Lindsay88,
  author = {Lindsay, P.A.},
  title = {A survey of mechanical support for formal reasoning},
  journal = {IEE/BCS Software Engineering Journal},
  month = {January},
  year = 1988,
  volume = 3,
  number = 1,
  pages = {3-27}
}

@inproceedings{jpb:Littlewood93,
  author = {Littlewood, B.},
  title = {The need for evidence from disparate sources to
    evaluate software safety},
  booktitle = {Directions in Safety-Critical Systems,
    Proc.\ Safety-Critical Systems Symposium, Bristol, UK},
  publisher = {Springer-Verlag},
  year = 1993
}

@book{jpb:LM91,
  editor = {Littlewood, B. and Miller, D.},
  title = {Software Reliability and Safety},
  publisher  = {Elsevier Applied Science},
  address = {London and New York},
  year = 1991,
  note = {Reprinted from
    {\em Reliability Engineering \& System Safety}, 32(1--2), 1989.},
  ISBN = {1-85166-533-1}
}

@article{jpb:LS92,
  author = {Littlewood, B. and Strigini, L.},
  title = {The risks of software},
  journal = {Scientific American},
  month = {November},
  year = 1992,
  volume = 267,
  number = 5,
  pages = {38-43}
}

@article{jpb:MacKenzie91a,
  author = {MacKenzie, D.},
  title = {The fangs of the {VIPER}},
  journal = {Nature},
  month = {8 August},
  year = 1991,
  volume = 352,
  pages = {467-468}
}

@techreport{jpb:MacKenzie91b,
  author = {MacKenzie, D.},
  title = {Negotiating arithmetic, constructing proof:
    the sociology of mathematics and information technology},
  type = {Programme on Information \& Communication Technologies,
    Working Paper Series},
  number = {No.\ 38},
  institution = {Research Centre for Social Sciences,
    University of Edinburgh},
  address = {56 George Square, Edinburgh EH8 9JU, UK},
  month = {November},
  year = 1991
}

@article{jpb:MH92,
  author = {Mahony, B. and Hayes, I.J.},
  title = {A case-study in timed refinement: A mine pump},
  journal = {IEEE Transactions on Software Engineering},
  volume = 18,
  number = 9,
  pages = {817-826},
  month = {September},
  year = 1992
}

@article{jpb:Malcolm92,
  author = {Malcolm, R.},
  title = {Safety critical systems research programme:
    technical workplan for the second phase},
  editor = {Redmill, F.},
  journal = {Safety Systems:
    The Safety-Critical Systems Club Newsletter},
  institution = {Centre for Software Reliability},
  address = {University of Newcastle upon Tyne, Newcastle NE1 7RU, UK},
  month = {January},
  year = 1992,
  volume = 1,
  number = 2,
  pages = {1-3}
}

@inproceedings{jpb:MMP92,
  author = {Maler, O. and Manna, Z. and Pnueli, A.},
  title = {From timed to hybrid systems},
  editor = {{de Bakker}, J.W. and Huizing, C. and {de Roever}, W.-P.
    and Rozenberg, G.},
  booktitle = {Real-Time: Theory in Practice},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 600,
  pages = {447-484},
  year = 1992
}

@book{jpb:MP92,
  author = {Manna, Z. and Pnueli, A.},
  title = {The Temporal Logic of Reactive and Concurrent Systems:
    Specification},
  publisher = {Springer-Verlag},
  year = 1992
}

@incollection{jpb:May90,
  author = {May, D.},
  title = {Use of formal methods by a silicon manufacturer},
  editor = {Hoare, C.A.R.},
  booktitle = {Developments in Concurrency and Communication},
  chapter = 4,
  publisher = {Addison-Wesley},
  series = {University of Texas at Austin Year of Programming Series},
  year = 1990,
  pages = {107-129}
}

@inproceedings{jpb:MF91,
  author = {Mayger, E.M. and Fourman, M.P.},
  title = {Integration of formal methods with system design},
  booktitle = {Proc.\ Conference on Very Large Scale Integration
    (VLSI'91), Edinburgh, UK},
  year = 1991,
  pages = {3a.2.1-3a.2.11}
}

@incollection{jpb:McDermid93,
  author = {McDermid, J.A.},
  title = {Formal methods: Use and relevance for the development of
    safety critical systems},
  editor = {Bennett, P.A.},
  booktitle = {Safety Aspects of Computer Control},
  publisher = {Butterworth-Heinemann Ltd},
  address = {Oxford, UK},
  ISBN = {0 7506 1102 2},
  year = 1993,
  other = {See also \cite{jpb:LM92}.}
}

@book{jpb:Bennett93,
  editor = {Bennett, P.A.},
  title = {Safety Aspects of Computer Control},
  publisher = {Butterworth-Heinemann Ltd},
  address = {Oxford, UK},
  ISBN = {0 7506 1102 2},
  price = {\pound 60},
  year = 1993
}

@article{jpb:M*89,
  author = {Moore, J.S. and others},
  title = {Special issue on system verification},
  journal = {Journal of Automated Reasoning},
  month = {December},
  year = 1989,
  volume = 5,
  number = 4,
  pages = {409-530}
}

@article{jpb:MM90,
  author = {Moser, L.E. and Melliar-Smith, P.M.},
  title = {Formal verification of safety-critical systems},
  journal = {Software -- Practice and Experience},
  month = {August},
  year = 1990,
  volume = 20,
  number = 8,
  pages = {799-821}
}

@techreport{jpb:NPL,
  author = {Mukherjee, P. and Stavridou, V.},
  title = {The formal specification of safety
    requirements for the storage of explosives},
  type = {Technical Report},
  number = {DITC 185/91},
  institution = {National Physical Laboratory},
  address = {Teddington, Middlesex TW11 0LW, UK},
  month = {August},
  year = 1991,
  other = {Published as \cite{jpb:MS93}.}
}

@article{jpb:MS93,
  author = {Mukherjee, P. and Stavridou, V.},
  title = {The formal specification of safety
    requirements for the storage of explosives},
  journal = {Formal Aspects of Computing},
  volume = 5,
  number = 4,
  pages = {299-336},
  year = 1993
}

@article{jpb:Myers86,
  author = {Myers, W.},
  title = {Can software for the strategic defense initiative
    ever be error-free?},
  journal = {IEEE Computer},
  month = {November},
  year = 1986,
  volume = 19,
  number = 11
}

@misc{jpb:SIFT:review,
  key = {NASA},
  title = {Peer review of a formal verification/design proof
    methodology},
  howpublished = {NASA Conference Publication 2377},
  month = {July},
  year = 1983
}

@inproceedings{jpb:NH92,
  author = {Natsume, T. and Hasegawa, Y.},
  title = {A View on Computer Systems and their Reliability in {Japan}},
  pages = {45-49},
  editor = {Frey, H.H.},
  booktitle = {Safety of computer control systems 1992 ({SAFECOMP'92}),
    Computer Systems in Safety-critical Applications,
    Proc.\ IFAC Symposium},
  location {Z\"urich, Switzerland, 28--30 October 1992},
  publisher = {Pergamon Press},
  year = 1992
}

@article{jpb:Neesham92,
  author = {Neesham, C.},
  title = {Safe conduct},
  journal = {Computing},
  month = {12 November},
  year = 1992,
  pages = {18-20}
}

@article{jpb:Neumann91,
  author = {Neumann, P.G.},
  other = {Editor},
  title = {Subsection on certification of professionals},
  journal = {ACM SIGSOFT Software Engineering Notes},
  month = {January},
  year = 1991,
  volume = 16,
  number = 1,
  pages = {24-32}
}

@article{jpb:Neumann91b,
  author = {Neumann, P.G.},
  title = {Certifying professionals},
  journal = {Communications of the ACM},
  month = {February 1991},
  volume = 34,
  number = 2,
  pages = 130
}

@article{jpb:Neumann92,
  author = {Neumann, P.G.},
  title = {Illustrative risks to the public in the use of computer
    systems and related technology},
  journal = {ACM SIGSOFT Software Engineering Notes},
  month = {January},
  year = 1992,
  volume = 16,
  number = 1,
  pages = {23-32},
  other = {List of risks cases as of 23 December 1991}
}

@inproceedings{jpb:Normington93,
  author = {Normington, G},
  title = {{Cleanroom} and {Z}},
  editor = {Bowen, J.P. and Nicholls, J.E.},
  booktitle = {Z User Workshop, London 1992},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {281-293},
  year = 1993
}

@book{jpb:Ono90,
  editor = {Ono, M.},
  title = {{Japanese} Perspectives in Software Engineering},
  publishers = {Addison Wesley},
  year = 1990
}

@article{jpb:Ostroff92,
  author = {Ostroff, J.S.},
  title = {Formal methods for the specification and design of
    real-time safety critical systems},
  journal = {Journal of Systems and Software},
  year = 1992,
  volume = 18,
  number = 1,
  pages = {33-60}
}

@incollection{jpb:Page91,
  author = {Page, I. and Luk, W.},
  title = {Compiling {Occam} into field-programmable gate arrays},
  editor = {Moore, W. and Luk, W.},
  booktitle = {FPGAs,
    Oxford Workshop on Field Programmable Logic and Applications},
  publisher = {Abingdon EE\&CS Books},
  address = {15 Harcourt Way, Abingdon OX14 1NV, UK},
  year = 1991,
  pages = {271-283}
}

@book{jpb:PS91,
  author = {Palfreman, J. and Swade, D.},
  title = {The Dream Machine},
  publisher = {BBC Books},
  address = {London, UK},
  year = 1991
}

@article{jpb:PSK90,
  author = {Parnas, D.L. and {von Schouwen}, A.J. and {Shu Po Kwan}},
  title = {Evaluation of safety-critical software},
  journal = {Communications of the ACM},
  month = {June},
  year = 1990,
  volume = 33,
  number = 6,
  pages = {636-648}
}

@article{jpb:PAM91,
  author = {Parnas, D.L. and Asmis, G.J.K. and Madey, J.},
  title = {Assessment of safety-critical software in
    nuclear power plants},
  journal = {Nuclear Safety},
  month = {April--June},
  year = 1991,
  volume = 32,
  number = 2,
  pages = {189-198}
}

@techreport{jpb:PM91,
  author = {Parnas, D.L. and Madey, J.},
  title = {Functional documentation for computer systems engineering},
  type = {CRL Report},
  number = {No.\ 237, Version 2},
  institution = {TRIO, Communications Research Laboratory},
  address = {Faculty of Engineering, McMaster University,
    Hamilton, Ontario, Canada L8S 4K1},
  month = {September},
  year = 1991
}

@inproceedings{jpb:PR92,
  author = {Pasquine, A. and Rizzo, A.},
  title = {Risk perceptions and acceptance of computers
    in critical applications},
  pages = {293-298},
  editor = {Frey, H.H.},
  booktitle = {Safety of computer control systems 1992 ({SAFECOMP'92}),
    Computer Systems in Safety-critical Applications,
    Proc.\ IFAC Symposium},
  location {Z\"urich, Switzerland, 28--30 October 1992},
  publisher = {Pergamon Press},
  year = 1992
}

@phdthesis{jpb:Pelaez88,
  author = {Pelaez, E.},
  title = {A gift from {Pandora}'s box: The software crisis},
  school = {Edinburgh University},
  address = {UK},
  year = 1988
}

@article{jpb:PBR90,
  author = {Pilling, M. and Burns, A. and Raymond, K.},
  title = {Formal specifications and proofs of inheritance protocols
    for real-time scheduling},
  journal = {IEE/BCS Software Engineering Journal},
  month = {September},
  year = 1990,
  volume = 5,
  number = 5,
  pages = {263-279}
}

@article{jpb:PDH91,
  author = {Probert, P.J. and Djian, D. and {Huosheng Hu}},
  title = {{Transputer} architectures for sensing in a robot
    controller: Formal methods for design},
  journal = {Concurrency: Practice and Experience},
  month = {August},
  year = 1991,
  volume = 3,
  number = 4,
  pages = {283-292}
}

@article{jpb:Pyle86,
  author = {Pyle, I.},
  title = {Software engineers and the {IEE}},
  journal = {IEE/BCS Software Engineering Journal},
  month = {March},
  year = 1986,
  volume = 1,
  number = 2,
  pages = {66-68}
}

@misc{jpb:Quintas90,
  author = {Quintas, P. and Hobday, M. and Guy, K.},
  title = {Evaluation of the {Alvey} software engineering programme},
  howpublished = {Science and Research Policy Unit,
    University of Sussex, Brighton, UK},
  month = {January},
  year = 1990
}

@inproceedings{jpb:RR91,
  author = {Ravn, A.P. and Rischel, H.},
  title = {Requirements Capture for Embedded Real-Time Systems},
  booktitle = {Proc.\ IMACS-MCTS'91 Symposium on Modelling
    and Control of Technological Systems},
  location = {Villeneuve d'Ascq, France, April 1991},
  volume = 2,
  year = 1991,
  pages = {147-152}
}

@incollection{jpb:RS93,
  author = {Ravn, A.P. and Stavridou, V.},
  title = {Project organisation},
  editor = {Bj\o{}rner, D. and Langmaack, H. and Hoare, C.A.R.},
  booktitle = {ProCoS I Final Deliverable},
  month = {January},
  year = 1993,
  publisher = {Department of Computer Science,
    Technical University of Denmark},
  address = {Lyngby, Denmark},
  note = {ProCoS Technical Report [ID/DTH DB 13/1]}
}

@book{jpb:Redmill88/89,
  author = {Redmill, F.},
  title = {Dependability of Critical Computer Systems,
    Volumes I and II},
  publisher = {Elsevier Applied Science},
  address = {London, UK},
  other = {Crown House, Linton Road, Barking, Essex, IG11 8JU, UK},
  year = {1988 and 1989}
}

@incollection{jpb:RF90,
  author = {Reade, C. and Froome, P.},
  title = {Formal methods for reliability},
  editor = {Rook, P.},
  booktitle = {Software Reliability Handbook},
  chapter = 3,
  publisher = {Elsevier Applied Science},
  year = 1990,
  pages = {51-81}
}

@book{jpb:Reason90,
  author = {Reason, J.},
  title = {Human Error},
  publisher = {Cambridge University Press},
  address = {UK},
  year = 1990
}

@misc{jpb:Risk92,
  key = {Royal Society},
  title = {Risk: Analysis, perception and management},
  howpublished = {The Royal Society,
    6 Carlton House Terrace, London SW1Y 5AG, UK},
  price = {\pounds15.50},
  year = 1992
}

@techreport{jpb:Rushby89,
  author = {Rushby, J. and Whitehurst, R.A.},
  title = {Formal verification of {AI} software},
  type = {Contractor Report},
  number = 181827,
  institution = {NASA Langley Research Center},
  address = {Hampton, Virginia, USA},
  month = {February},
  year = 1989
}

@techreport{jpb:Rushby91,
  author = {Rushby, J.},
  title = {Formal specification and verification of a fault-masking and
    transient-recovery model for digital flight control systems},
  type = {Technical Report},
  number = {SRI-CSL-91-3},
  institution = {SRI International},
  address = {Menlo Park, California, USA},
  month = {January},
  year = 1991,
  note = {Also available as NASA Contractor Report 4384.}
}

@techreport{jpb:RHO91,
  author = {Rushby, J. and {von Henke}, F. and Owre, S.},
  title = {An introduction to formal specification and verification
    using {EHDM}},
  type = {Technical Report},
  number = {SRI-CSL-91-02},
  institution = {SRI International},
  address = {Menlo Park, California, USA},
  month = {February},
  year = 1991
}

@article{jpb:RH93,
  author = {Rushby, J. and {von Henke}, F.},
  title = {Formal verification of algorithms for critical systems},
  journal = {IEEE Transactions on Software Engineering},
  volume = 19,
  number = 1,
  pages = {13-23},
  month = {January},
  year = 1993
}

@techreport{jpb:Scholefield90,
  author = {Scholefield, D.J.},
  title = {The formal development of real-time systems: A review},
  type = {Technical Report},
  number = {YCS 145},
  institution = {Department of Computer Science, University of York},
  address = {UK},
  year = 1990
}

@article{jpb:SBB87,
  author = {Selby, R.W. and Basili, V.R. and Baker, F.T.},
  title = {{Cleanroom} software development: An empirical evaluation},
  journal = {IEEE Transactions on Software Engineering},
  volume = 13,
  number = 9,
  pages = {1027-1037},
  month = {September},
  year = 1987
}

@book{jpb:Sennett89,
  editor = {Sennett, C.T.},
  title = {High-Integrity Software},
  publisher = {Pitman},
  series = {Computer Systems Series},
  year = 1989
}

@inproceedings{jpb:STP,
  author = {Shostak, R.E. and Schwartz, R. and Melliar-Smith, P.M.},
  title = {{STP}: A mechanized logic for specification
    and verification},
  editor = {D.W. Loveland},
  booktitle = {6th Conference on Automated Deduction
    (CADE-6)},
  publisher = {Springer-Verlag},
  series = LNCS,
  year = 1982,
  volume = 138
}

@article{jpb:Smith70,
  author = {Smith, C.L.},
  title = {Digital control of industrial processes},
  journal = {ACM Computing Surveys},
  year = 1970,
  volume = 2,
  number = 3,
  pages = {211-241}
}

@book{jpb:SW89,
  author = {Smith, D.J. and Wood, K.B.},
  title = {Engineering Quality Software:
    a review of current practices, standards and guidelines
    including new methods and development tools},
  edition = {2nd},
  publisher = {Elsevier Applied Science},
  year = 1989
}

@book{jpb:Sommerville92,
  author = {I. Sommerville},
  title = {Software Engineering},
  publisher = {Addison-Wesley},
  edition = {4th},
  ISBN = {0-201-56529-3},
  year = 1992
}

@techreport{jpb:SNH91,
  author = {S{\o}rensen, E.V. and Nordahl, J. and Hansen, N.H.},
  title = {From {CSP} models to {Markov} models: A case study},
  number = {ID-TR:1991-92},
  institution = {Department of Computer Science,
    Technical University of Denmark},
  address = {Lyngby, Denmark},
  year = 1991
}

@article{jpb:Spectrum,
  author = {{IEEE Spectrum}},
  title = {Special issue on reliability},
  journal = {IEEE Spectrum},
  month = {October},
  year = 1981,
  volume = 18,
  number = 10
}

@article{jpb:Spivey90,
  author = {Spivey, J.M.},
  title = {Specifying a real-time kernel},
  journal = {IEEE Software},
  month = {September},
  year = 1990,
  pages = {21-28}
}

@book{jpb:Z,
  author = {Spivey, J.M.},
  title = {The {Z} Notation: A Reference Manual},
  edition = {2nd},
  publisher = {Prentice Hall
    International Series in Computer Science},
  ISBN = {13-978529-9},
  year = 1992
}

@techreport{jpb:Srivas91,
  author = {Srivas, M. and Bickford, M.},
  title = {Verification of the FtCayuga fault-tolerant
    microprocessor system,
    vol 1: A case study in theorem prover-based verification},
  type = {Contractor Report},
  number = 4381,
  institution = {NASA Langley Research Centre},
  address = {Hampton, Virginia, USA},
  month = {July},
  year = 1991,
  note = {Work performed by ORA corporation.)}
}

@article{jpb:Stein92a,
  author = {Stein, R.M.},
  title = {Safety by formal design},
  journal = {BYTE},
  month = {August},
  year = 1992,
  pages = 157
}

@book{jpb:Stein92b,
  author = {Stein, R.M.},
  title = {Software Safety},
  booktitle = {Real-time Multicomputer Software Systems},
  chapter = 5,
  publisher = {Ellis-Horwood},
  year = 1992,
  pages = {109-133}
}

@book{jpb:SBC92,
  editor = {Stepney, S. and Barden, R. and Cooper, D.},
  title = {Object Orientation in {Z}},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  year = 1992
}

@book{jpb:Swade91,
  author = {Swade, D.},
  title = {{Charles Babbage} and his Calculating Engines},
  publisher = {Science Museum},
  address = {London, UK},
  year = 1991
}

@inproceedings{jpb:Thomas88,
  author = {Thomas, M.C.},
  title = {The future of formal methods},
  editor = {Bowen, J.P.},
  booktitle = {Proc.\ 3rd Annual Z Users Meeting},
  publisher = {Oxford University Computing Laboratory},
  address = {UK},
  month = {December},
  year = 1988,
  pages = {1-3}
}

@article{jpb:Thomas89,
  author = {Thomas, M.C.},
  title = {Development methods for trusted computer systems},
  journal = {Formal Aspects of Computing},
  year = 1989,
  volume = 1,
  number = {1},
  pages = {5-18}
}

@inproceedings{jpb:Tierney91a,
  author = {Tierney, M.},
  title = {The evolution of {Def Stan} 00-55 and 00-56:
    an intensification of the ``formal methods debate'' in the {UK}},
  booktitle = {Proc.\ Workshop on Policy Issues in Systems
    and Software Development},
  publisher = {Science Policy Research Unit},
  address = {Brighton, UK},
  month = {July},
  year = 1991
}

@misc{jpb:Tierney91b,
  author = {Tierney, M.},
  title = {Some implications of {Def Stan} 00-55 on the software
    engineering labour process in safety critical developments},
  howpublished = {Research Centre for Social Sciences,
    Edinburgh University, UK},
  year = 1991
}

@book{jpb:vonNeumann61,
  author = {{von Neumann}, J.},
  title = {Probabilistic logics and synthesis of reliable organisms
    from unreliable components},
  booktitle = {Collected Works},
  volume = 5,
  publisher = {Pergamon Press},
  year = 1961
}

@inproceedings{jpb:Waldinger91,
  author = {Waldinger, R.J. and Stickel, M.E.},
  title = {Proving properties of rule-based systems},
  booktitle = {Proc.\ 7th Conference on Artificial Intelligence
    Applications, Miami Beach, Florida, USA},
  publisher = {IEEE Computer Society},
  month = {February},
  year = 1991,
  pages = {81-88}
}

@techreport{jpb:WKC91,
  author = {Wallace, D.R. and Kuhn, D.R. and Cherniavsky, J.C.},
  title = {Report of the {NIST} workshop of standards for the assurance
    of high integrity software},
  type = {NIST Special Publication},
  number = {500-190},
  institution = {Computer Systems Laboratory,
    National Institute of Standards and Technology},
  address = {Gaithersburg, MD 20899, USA},
  month = {August},
  year = 1991,
  note = {Available from the Superintendent of Documents,
    Government, U.S. Printing Office, Washington, DC 20402, USA.}
}

@article{jpb:WKI92,
  author = {Wallace, D.R. and Kuhn, D.R. and Ippolito, L.M.},
  title = {An analysis of selected software safety standards},
  journal = {IEEE AES Magazine},
  month = {August},
  year = 1992,
  pages = {3-14}
}

@article{jpb:Ward91,
  author = {Ward, W.T.},
  title = {Calculating the real cost of software defects},
  journal = {Hewlett-Packard Journal},
  month = {October},
  year = 1991,
  pages = {55-58}
}

@incollection{jpb:Webb91,
  author = {Webb, J.T.},
  title = {The role of verification and validation
    tools in the production of critical software},
  editor = {Ince, D.},
  booktitle = {Software Quality and Reliability: Tools and Methods},
  note = {Unicorn Applied Info Technology reports 6},
  chapter = 4,
  publisher = {Chapman \& Hall},
  address = {London, UK},
  year = 1991,
  pages = {33-41}
}

@article{jpb:SIFT,
  author = {Wensley, J. and others},
  title = {{SIFT}: Design and analysis of a fault-tolerant
    computer for aircraft control},
  journal = {Proc.\ IEEE},
  year = 1978,
  volume = 60,
  number = 10,
  pages = {1240-1254}
}

@article{jpb:Wirth77,
  author = {Wirth, N.},
  title = {Towards a discipline of real-time programming},
  journal = {Communications of the ACM},
  month = {August},
  year = 1977,
  volume = 20,
  number = 8,
  pages = {577-583}
}

@book{jpb:Wichmann92,
  editor = {Wichmann, B.A.},
  title = {Software in Safety-Related Systems},
  publisher = {John Wiley \& Sons},
  year = 1992,
  note = {Also published by BCS},
  ISBN = {0-471-934747}
}

@techreport{jpb:WZ91,
  author = {Wright, C.L. and Zawilski, A.J.},
  title = {Existing and emerging standards for software safety},
  institution = {The MITRE Corporation,
    Center for Advanced Aviation System Development},
  address = {7525 Colshire Drive, McLean, Virginia 22102-3481, USA},
  type = {Ref.},
  number = {MP-91W00028},
  month = {June},
  year = 1991,
  note = {Presented at the
    IEEE Fourth Software Engineering Standards Application Workshop,
    San Diego, California, USA, 20--24 May 1991.}
}

@manual{jpb:Xilinx91,
  key = {Xilinx},
  title = {The Programmable Gate Array Data Book},
  organization = {{Xilinx, Inc.}},
  address = {San Jose, California, USA},
  year = 1991
}

@misc{jpb:Youll88,
  author = {Youll, D.P.},
  title = {Study of the training and education needed in
    support of {Def Stan} 00-55},
  howpublished = {Cranfield IT Institute Ltd, UK},
  month = {September},
  year = 1988,
  note = {Also an appendix of the April 1989 00-55 draft.}
}

@article{jpb:ZHR91,
  author = {{Zhou Chaochen} and Hoare, C.A.R. and Ravn, A.P.},
  title = {A calculus of durations},
  journal = {Information Processing Letters},
  year = 1991,
  volume = 40,
  number = 5,
  pages = {269-276}
}

@incollection{jpb:Sommerville92b,
  author = {I. Sommerville},
  title = {Software Safety},
  booktitle = {Software Engineering},
  chapter = {21},
  pages = {407-424},
  publisher = {Addison-Wesley},
  edition = {4th},
  year = 1992
}

@book{jpb:RA93a,
  editor = {F. Redmill and T. Anderson},
  title = {Safety-Critical Systems:
    Current Issues, Techniques and Standards},
  publisher = {Chapman \& Hall},
  address = {London, UK},
  ISBN = {0-412-54820-8},
  year = 1993
}

@proceedings{jpb:RA93,
  editor = {F. Redmill and T. Anderson},
  title = {Directions in Safety-Critical Systems,
    Proc.\ Safety-Critical Systems Symposium, Bristol, UK},
  publisher = {Springer-Verlag},
  ISBN = {3-540-19817-2},
  month = {February},
  year = 1993
}

@techreport{jpb:JR91,
  author = {M.B. Josephs and D. Redmund-Pyle},
  title = {Entity-relationship models expressed in {Z}:
    a synthesis of structured and formal methods},
  type = {Technical Report},
  number = {PRG-TR-20-91},
  institution = {Programming Research Group,
    Oxford University Computing Laboratory},
  address = {UK},
  month = {July},
  year = 1991
}

@incollection{jpb:MBS92,
  author = {D. May and G. Barrett and D. Shepherd},
  title = {Designing chips that work},
  pages = {3-19},
  editor = {Hoare, C.A.R. and Gordon, M.J.C.},
  booktitle = {Mechanized Reasoning and Hardware Design},
  publisher = {Prentice Hall
    International Series in Computer Science},
  year = 1992
}

@inproceedings{jpb:WZ91b,
  author = {J.M. Wing and A.M. Zaremski},
  title = {Unintrusive ways to integrate formal specifications
    in practice},
  editor = {Prehn, S. and Toetenel, W.J.},
  booktitle = {VDM'91: Formal Software Development Methods, Volume 1},
  publisher = {Springer-Verlag},
  series = LNCS,
  year = 1991,
  volume = 551,
  pages = {547-569}
}

@article{jpb:MacKenzie92,
  author = {MacKenzie, D.},
  title = {Computers, formal proof, and the law courts},
  journal = {Notices of the American Mathematical Society},
  volume = 39,
  number = 9,
  month = {November},
  year = 1992,
  pages = {1066-1069}
}

@article{jpb:Potocki93,
  author = {{Potocki de Montalk}, J.P.},
  title = {Computer software in civil aircraft},
  journal = {Microprocessors and Microsystems},
  editor = {Cullyer, W.J.},
  other = {Special issue on safety critical systems},
  volume = 17,
  number = 1,
  pages = {17-23},
  month = {January/February},
  year = 1993
}

@article{jpb:Thomas93,
  author = {Thomas, M.C.},
  title = {The industrial use of formal methods},
  journal = {Microprocessors and Microsystems},
  editor = {Cullyer, W.J.},
  other = {Special issue on safety critical systems},
  volume = 17,
  number = 1,
  pages = {31-36},
  month = {January/February},
  year = 1993
}

@book{jpb:Pyle91,
  author = {Pyle, I.C.},
  title = {Developing Safety Systems: A guide using {Ada}},
  publisher = {Prentice Hall},
  ISBN = {0-13-204298-3},
  year = 1991
}

@techreport{jpb:WIK92,
  author = {Wallace, D.R. and Ippolito, L.M. and Kuhn, D.R.},
  title = {High Integrity Software Standards and Guidelines},
  type = {NIST Special Publication},
  number = {500-204},
  institution = {Computer Systems Technology,
    U.S.\ Department of Commerce,
    National Institute of Standards and Technology},
  address = {Gaithersburg, MD 20899, USA},
  month = {September},
  year = 1992,
  note = {Available from the Superintendent of Documents,
    Government, U.S. Printing Office, Washington, DC 20402, USA.}
}

@article{jpb:LN93,
  author = {Leveson, N.G. and Neumann, P.G.},
  title = {Introduction to Special Issue on Software for
    Critical Systems},
  journal = {IEEE Transactions on Software Engineering},
  volume = 19,
  number = 1,
  pages = {1-2},
  month = {January},
  year = 1993
}

@techreport{jpb:PWT90,
  author = {P.R.H. Place and W.G. Wood and M. Tudball},
  title = {Survey of Formal Specification Techniques for
    Reactive Systems},
  type = {Technical Report},
  institution = {Software Engineering Institute},
  address = {Carnegie-Mellon University, Pittsburgh, PA, USA},
  year = 1990
}

@inproceedings{jpb:KPS93,
  author = {M.R.K. {Krishna Rao} and P.K. Pandya and R.K. Shyamasunder},
  title = {Verification Tools in the Development of
    Provably Correct Compilers},
  editor = {Woodcock, J.C.P. and Larsen, P.G.},
  booktitle = {FME'93: Industrial-Strength Formal Methods},
  location = {Odense, Denmark, 19--23 April 1993},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 670,
  pages = {442-461},
  year = 1993,
}

@article{jpb:Bowen*93,
  author = {J.P. Bowen and others},
  title = {A {ProCoS II} Project Description:
    {ESPRIT Basic Research} Project 7071},
  journal = {Bulletin of the European Association for Theoretical
    Computer Science (EATCS)},
  ISSN = {0252-9742},
  volume = 50,
  month = {June},
  year = 1993,
  pages = {128-137}
}

@article{jpb:BS93b,
  author = {J.P. Bowen and V. Stavridou},
  title = {Safety-Critical Systems, Formal Methods and Standards},
  journal = {IEE/BCS Software Engineering Journal},
  volume = 8,
  number = 4,
  pages = {189-209},
  month = {July},
  year = {1993},
  other = {Also available in an older version as
    Oxford University Computing Laboratory
    Technical Report PRG-TR-5-92.}
}

@inproceedings{jpb:Olderog92,
  author = "E.-R. Olderog",
  title = "Interfaces between Languages for Communicating Systems",
  editor = "W. Kuich",
  booktitle = "Automata, Languages and Programming (ICALP'92)",
  other = "Proc.\ 19th International Colloquium,
    Wien, Austria, July 1992",
  publisher = Springer,
  series = LNCS,
  volume = 623,
  year = 1992
}

@inproceedings{jpb:Bowen93b,
  author = {J.P. Bowen},
  title = {Formal Methods in Safety-Critical Standards},
  booktitle = {Proc.\ 1993 Software Engineering Standards Symposium},
  other = {SESS'93},
  publisher = {IEEE Computer Society Press},
  location = {Brighton, UK, 30 August -- 3 September},
  pages = {168-177},
  year = 1993
}

@incollection{jpb:HH92,
  author = {C.A.R. Hoare and {He Jifeng}},
  title = {Refinement algebra proves correctness of a compiler},
  editor = {M. Broy},
  booktitle = {Programming and Mathematical Method:
    International Summer School directed by
    F.L.\ Bauer, M.\ Broy, E.W.\ Dijkstra, C.A.R.\ Hoare},
  series = {NATO ASI Series F: Computer and Systems Sciences},
  volume = 88,
  publisher = Springer,
  ISBN = {3-540-55558-7},
  pages = {245-269},
  year = 1992
}

@book{jpb:CSP,
  author = {C.A.R. Hoare},
  title = {Communicating Sequential Processes},
  publisher = {Prentice Hall International
    Series in Computer Science},
  year = 1985
}

@article{jpb:Roscoe88,
  author = {A.W. Roscoe and C.A.R. Hoare},
  title = {Laws of {Occam} Programming},
  journal = {Theoretical Computer Science},
  volume = 60,
  pages = {177-229},
  year = 1988
}

@techreport{jpb:Bowen87a,
  author = {J.P. Bowen},
  title = {The Formal Specification of a Microprocessor
    Instruction Set},
  institution = oucl,
  address = uk,
  type = {Technical Monograph},
  number = {PRG-60},
  length = {72},
  month = {January},
  year = {1987},
  isbn = {0-902928-42-2},
  annote = {The Z notation is used to define the Motorola M6800 8-bit
    microprocessor instruction set.}
}

@article{Z:Bowen87b,
  author = {J.P. Bowen},
  editor = {H. Schumny and J. M{\o}lgaard},
  title = {Formal Specification and Documentation of Microprocessor
    Instruction Sets},
  booktitle = {Proc.\ EUROMICRO'87,
    Microcomputers: Usage, Methods and Structures},
  journal = {Microprocessing and Microprogramming},
  publisher = {Elsevier Science Publishers},
  organization = {EUROMICRO},
  location = {Portsmouth, UK, 14--17 September 1987},
  volume = {21},
  pages = {223-230},
  length = {690},
  month = {August},
  year = {1987}
}

@inproceedings{jpb:Bowen88,
  author = {J.P. Bowen},
  title = {Formal Specification in {Z} as a Design and
    Documentation Tool},
  booktitle = {Proc.\ Second {IEE}/{BCS} Conference
    on Software Engineering},
  organization = {IEE/BCS},
  location = {Liverpool, UK, July 1988},
  volume = {290},
  pages = {164-168},
  month = {July},
  year = {1988}
}

@inproceedings{jpb:Bowen93a,
  author = {J.P. Bowen},
  title = {Select {Z} Bibliography},
  booktitle = {{Z} User Workshop, {London} 1992},
  editor = {J.P. Bowen and J.E. Nicholls},
  publisher = Springer,
  series = WICS,
  pages = {309-341},
  year = 1993
}

@inproceedings{jpb:Gordon91,
  author = {M.J.C. Gordon},
  title = {A Formal Method for Hard Real-Time Programming},
  editor = {J.M. Morris and R.C. Shaw},
  booktitle = {Proc.\ 4th Refinement Workshop},
  publisher = Springer,
  series = WICS,
  year = 1991
}

@article{jpb:HCH93,
  author = {R.W.S. Hale and R. Cardell-Oliver and J.M.J. Herbert},
  title = {An Embedding of Timed Transition Systems in {HOL}},
  journal = {Formal Methods in System Design},
  volume = 3,
  number = {1 \& 2},
  month = {September},
  publisher = {Kluwer Academic Publishers},
  year = 1993
}

@article{jpb:HB93,
  author = {{He Jifeng} and J.P. Bowen},
  title = {Specification, Verification and Prototyping
    of an Optimized Compiler},
  journal = {Formal Aspects of Computing},
  year = {to appear}
}

@techreport{jpb:CGM86,
  author = {A. Camilleri and M.J.C. Gordon and T. Melham},
  title = {Hardware Verification using {Higer-Order Logic}},
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  number = 91,
  month = {September},
  year = 1986
}

@techreport{jpb:Gordon88,
  author = {M.J.C. Gordon},
  title = {Mechanizing Programming Logics in {Higher Order Logic}},
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  number = 145,
  month = {September},
  year = 1988
}

@techreport{jpb:Leonard90,
  author = {T.E. Leonard},
  title = {Specification of computer architectures:
    A survey and annotated bibliography},
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  number = 188,
  month = {January},
  year = 1990
}

@techreport{jpb:BGHvT90,
  author = {R. Boulton and M.J.C. Gordon and J.M.J. Herbert
    and J. {van Tassel}},
  title = {The {HOL} Verification of {ELLA} Designs},
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  number = 199,
  month = {August},
  year = 1990
}

@techreport{jpb:Camilleri91,
  author = {J.A. Camilleri},
  title = {Symbolic compilation and execution of programs by proof:
    A case study in {HOL}},
  institution = {University of Cambridge, Computer Laboratory},
  address = {UK},
  number = 240,
  month = {December},
  year = 1991
}

@book{jpb:book,
  editor = {J.P. Bowen},
  title = {Towards Verified Systems},
  publisher = {Elsevier Science Publishers},
  series = {Real-Time Safety Critical Systems Series},
  year = 1993,
  note = {In preparation}
}

@article{jpb:Shepherd90,
  author = {D.E. Shepherd},
  title = "Verified microcode design",
  journal = "Microprocessors and Microsystems",
  volume = 14,
  number = 10,
  pages = "623-630",
  publisher = "North-Holland",
  year = 1990
}

@article{jpb:SW89b,
  author = {D.E. Shepherd and G. Wilson},
  title = {Making Chips that Work},
  journal = {New Scientist},
  volume = {1664},
  pages = {61-64},
  month = {May},
  year = {1989},
  annote = {A general article containing information on the
    formal development of the T800 floating-point unit for the
    transputer including the use of Z.}
}

@techreport{jpb:CGR93a,
  author = {Craigen, D. and Gerhart, S. and Ralston, T.J.},
  title = {An International Survey of Industrial Applications of
    Formal Methods
    (Volume 1: Purpose, Approach, Analysis and Conclusions,
     Volume 2: Case Studies)},
  institution = {Atomic Energy Control Board of Canada,
    U.S.\ National Institute of Standards and Technology,
    and U.S.\ Naval Research Laboratories},
  address = {National Technical Information Service,
    5285 Port Royal Road, Springfield, VA 22161, USA},
  number = {NIST GCR 93/626-V1 \& NIST GCR 93-626-V2
    (Order numbers: PB93-178556/AS \& PB93-178564/AS)},
  other = {Phone: +1-703-487-4650},
  year = 1993
}

@inproceedings{jpb:CGR93b,
  author = {Craigen, D. and Gerhart, S. and Ralston, T.J.},
  title = {Formal methods reality check: Industrial usage},
  editor = {Woodcock, J.C.P. and Larsen, P.G.},
  booktitle = {FME'93: Industrial-Strength Formal Methods},
  location = {Odense, Denmark, 19--23 April 1993},
  publisher = {Springer-Verlag},
  series = LNCS,
  volume = 670,
  pages = {250-267},
  year = 1993,
}

@techreport{jpb:AP93,
  author = "S. Austin and G.I. Parkin",
  title = "Formal Methods: A Survey",
  institution = "National Physical Laboratory",
  address = {Queens Road, Teddington, Middlesex, TW11 0LW, UK},
  month = "March",
  year = "1993"
}

@techreport{jpb:PK93,
  author = {P.R.H. Place and K.C. Kang},
  title = {Safety-Critical Software:
    Status Report and Annotated Bibliography},
  number = {CMU/SEI-92-TR-5 \& ESC-TR-93-182},
  institution = {Software Engineering Institute},
  address = {Carnegie Mellon University,
    Pittsburgh, Pennsylvania 15213, USA},
  month = {June},
  year = 1993
}

@inproceedings{jpb:HPB93,
  author = {{He Jifeng} and I. Page and J.P. Bowen},
  title = {Towards a provably correct hardware implementation of
    {Occam}},
  editor = {G.J. Milne and L. Pierre},
  booktitle = {Correct Hardware Design and Verification Methods
    (CHARME'93)},
  other = {Proc.\ IFIP WG10.2 Advanced Research Working Conference},
  location = {Arles, France, 24--26 May 1993},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 683,
  pages = {214-225},
  year = 1993,
  other = {Based on ProCoS document [OU HJF 9]}
}

@inproceedings{apr:BHP90,
  author = {J.P. Bowen and {He Jifeng} and P.K. Pandya},
  title = {An Approach to Verifiable Compiling
    Specification and Prototyping},
  editor = {P. Deransart and J. Ma\l{}uszy\'nski},
  booktitle = {Programming Language Implementation and
    Logic Programming},
  other = {International Workshop PLILP'90},
  location = {Link\"oping, Sweden, 20--22 August 1990},
  publisher = Springer,
  series = LNCS,
  volume = 456,
  pages = {45-59},
  year = 1990
}

@article{apr:Bowen91,
  author = "J.P. Bowen",
  title = {From Programs to Object Code and back again using
    Logic Programming: Compilation and Decompilation},
  journal = {Journal of Software Maintenance: Research and Practice},
  other = {Based on ESPRIT II REDO project document 2487-TN-PRG-1044,
    Oxford University Computing Laboratory, UK, 1991.},
  volume = 5,
  number = 4,
  pages = {205-234},
  month = dec,
  year = "1993"
}

@inproceedings{apr:Bowen92,
  author = {J.P. Bowen},
  title = {From Programs to Object Code using Logic
    and Logic Programming},
  editor = {R. Giegerich and S.L. Graham},
  booktitle = {Code Generation -- Concepts, Tools, Techniques,
      Proc.\ International Workshop on Code Generation},
  location = {Dagstuhl, Germany, 20--24 May 1991},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {173-192},
  year = {1992}
}

@techreport{apr:BBOR93,
  author = "J.P. Bowen and B. Buth and E.-R. Olderog and A.P. Ravn",
  title = "{Provably Correct Systems}, Tutorial Material for {Formal
    Methods Europe} '93",
  institution = "Department of Computer Science,
    Technical University of Denmark",
  address = "DK-2800 Lyngby, Denmark",
  type = "ProCoS Technical Report",
  number = "[ID/DTH~APR~20/1]",
  month = "March",
  year = 1993
}

@inproceedings{apr:BFOR93,
  author =  {J.P. Bowen and M. Fr\"anzle and E.-R. Olderog
    and A.P. Ravn},
  title = {Developing Correct Systems},
  booktitle = {Proc.\ 5th Euromicro Workshop on Real-Time Systems},
  publisher = {IEEE Computer Society Press},
  location = {Oulu, Finland, 22--24 June 1993},
  pages = {176-187},
  year = 1993
}

@inproceedings{apr:BBF*92,
  author = {B. Buth and K.-H. Buth and  M. Fr\"anzle and
    B. {von Karger} and Y. Lakhneche and H. Langmaack and
    M. M\"uller-Olm},
  title = "Provably Correct Compiler Implementation",
  booktitle = "Compiler Construction (CC'92)",
  other = {4th Int.\ Conf.\ CC'92},
  location = {Paderborn, Germany, 1992},
  editor = "U. Karstens and P. Pfahler",
  publisher = Springer,
  series = LNCS,
  volume = 641,
  pages = "141-155",
  year = 1992
}

@inproceedings{apr:HB92,
  author = "{He Jifeng} and J.P. Bowen",
  title = "Time Interval semantics and Implementation of a Real-Time
    Programming Language",
  booktitle = "Proc.\ 4th Euromicro Workshop on Real-Time Systems",
  pages = "110-115",
  publisher = "IEEE Computer Society Press",
  location = {Athens, Greece, 3--5 June, 1992},
  year = 1992
}

@inproceedings{apr:Hoare91,
  author = "C.A.R. Hoare",
  title = "Refinement algebra proves correctness of compiling
    specifications",
  booktitle = "3rd Refinement Workshop",
  editor = "C.C. Morgan and J.C.P. Woodcock",
  pages = "33-48",
  publisher = Springer,
  series = WICS,
  year = 1991
}

@inproceedings{apr:Nordahl92,
  author = "J. Nordahl",
  title = "Design for dependability",
  booktitle = "Proc.\ 3rd IFIP Working Conference on
    Dependable Computing for Critical Applications",
  other = "Mondello, Italy, September 1992",
  series = "Dependable Computing and Fault-Tolerant Computing Series",
  publisher = Springer,
  year = 1992
}

@techreport{apr:Parnas,
  author = "D.L. Parnas and G.J.K. Asmis and J. Madey",
  title = "Assessment of Safety-critical Software",
  institution = "TRIO, Queen's University",
  address = "Kingston, Canada",
  number = "Technical Report 90-295",
  month = "December",
  year = 1990
}

@inproceedings{apr:Pnueli88,
  author = "A. Pnueli and E. Harel",
  title = "Applications of Temporal Logic to the Specification
    of Real-Time Systems (extended abstract)",
  booktitle = "Formal Techniques in
    Real-Time and Fault-Tolerant Systems",
  editor  = "M. Joseph",
  series  = LNCS,
  volume  = 331,
  publisher = Springer,
  year = 1988,
  pages = "84-98"
}

@inproceedings{apr:RS90,
  author = {A.P. Ravn and H. Rischel and V. Stavridou},
  title = {Provably Correct Safety Critical Software},
  booktitle = {Proc.\ IFAC Safety of Computer Controlled Systems 1990
    (SAFECOMP'90)},
  publisher = {Pergamon Press},
  annote = {Also available as Technical Report CSD-TR-625,
    Dept.\ of Computer Science, Royal Holloway, University of London,
    Egham, Surrey TW20 0EX, UK.},
  year = {1990}
}

@article{apr:RRH93,
  author = "A.P. Ravn and H. Rischel and K.M. Hansen",
  title = "Specifying and Verifying Requirements of Real-Time Systems",
  journal = "IEEE Transactions on Software Engineering",
  volume = "19",
  number = 1,
  pages = "41-55",
  month = "January",
  year = "1993"
}

@inproceedings{apr:SRRZ92,
  author = "J.U. Skakkeb{\ae}k and A.P. Ravn and H. Rischel
    and {Zhou Chaochen}",
  title = "Specification of embedded real-time systems",
  booktitle = "Proc.\ 4th Euromicro Workshop on Real-Time Systems",
  pages = "116-121",
  publisher = "IEEE Computer Society Press",
  location = {Athens, Greece, 3--5 June, 1992},
  year = 1992
}

@article{apr:SRL91,
  author = "J.F. S\o{}gaard-Andersen and C.O. Rump
    and H.H. L\o{}vengreen",
  title = "A Systematic Kernel Development",
  booktitle = "Proc.\ ACM SIGSOFT'91 Conference on
    Software for Critical Systems, New Orleans, US",
  journal = "ACM Software Engineering Notes",
  volume = 16,
  number = 5,
  pages = "55-65",
  publisher = "ACM",
  year = 1991
}

@article{apr:SNH92,
  author = "E.V. S{\o}rensen and J. Nordahl and N.H. Hansen",
  title = "From {CSP} models to {Markov} models",
  journal = "IEEE Transactions on Software Engineering",
  year = "to appear"
}
% Was 1992

@inproceedings{apr:ZHRR91,
  author = "{Zhou Chaochen} and M.R. Hansen and A.P. Ravn and
    H. Rischel",
  title = "Duration Specifications for Shared Processors",
  booktitle = "Formal Techniques in Real-Time and
    Fault-Tolerant Systems",
  editor = "J. Vytopil",
  series = LNCS,
  volume = 571,
  pages = "21-32",
  publisher = Springer,
  year = 1991
}

@book{apr:Zwi89,
  author = "J. Zwiers",
  title = "Compositionality, Concurrency and Partial Correctness",
  subtitle = {Proof Theories for Networks of Processes and
    their Relationship},
  series = LNCS,
  volume = 321,
  publisher = Springer,
  year = 1989
}

@book{jpb:Neumann94,
  author = {P. G. Neumann},
  title = {Computer-Related Risks},
  publisher = {Addison-Wesley},
  price = {$24.75},
  ISBN = {0-201-55805-X},
  length = 384,
  year = 1994
}

@book{jpb:Leveson94,
  author = {N. G. Leveson},
  title = {Safeware: System Safety in the Computer Age},
  publisher = {Addison-Wesley},
  year = 1994,
  note = {To appear}
}

@article{jpb:Gibbs94,
  author = {W. W. Gibbs},
  title = {Software's Chronic Crisis},
  journal = {Scientific American},
  volume = 271,
  number = 3,
  page = {86-95},
  month = sep,
  year = 1994
}