Virtual Library Software Engineering Formal Methods

Formal Methods Publications

• Introduction
• Bibliographies
• Collections of Technical Reports, etc.
• Journals
• Individual books
• Selected papers

Introduction

J.M. Wing, A Specifier's Introduction to Formal Methods. IEEE Computer, 23(9):8-24, September 1990.

J.A. Hall, Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990.

J.P. Bowen and M.G. Hinchey, Seven More Myths of Formal Methods. IEEE Software, 12(4):34-41, July 1995.

For general background reading on the need for formal methods, This article recommends the WWW formal methods page for further reading, see:

W.W. Gibbs, Software's Chronic Crisis. Scientific American, 271(3):86-95, September 1994.

M.D. Faser, K. Kumar and V.K. Vaishnavi, Strategies for Incorporating Formal Specifications in Software Development. CACM, 37(10):74-86, October 1994.

J.P. Bowen and M.G. Hinchey, Ten Commandments of Formal Methods. IEEE Computer, 28(4):56-63, April 1995.

H. Saiedian (ed.), An Invitation to Formal Methods. IEEE Computer, 29(4):16-30, April 1996.

P.G. Larsen, J. Fitzgerald and T. Brookes, Applying Formal Specification in Industry. IEEE Software, 13(7):48-56, May 1996.

E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996. (22 pages, 123 references.)

Bibliographies

• Bibliographies on Software/Hardware Engineering and Formal Methods from a large Collection of Computer Science Bibliographies. Search for publications on formal methods. Includes searchable versions of the B-Method, FACS, FME, hardware verification, introductory material for formal methods, Larch, ProCoS II, RAISE, software reuse, VDM, VDM++, VHDL verification, Z notation and contributed bibliographies. See also Theory/Foundations of Computer Science section, including Calculi for Mobile Processes (Pi calculus).

• Canadian mirror site for Bibliographies on Software/Hardware Engineering and Formal Methods from The Collection of Computer Science Bibliographies.

• Formal methods introductory material by Peter Gorm Larsen. See also Formal Methods Europe and VDM Symposia bibliography and other related bibliography material.

• Recent Books on Formal Methods, C.B. Jones, 1995.

• Formal Methods - Selected Historical References, C.B. Jones and A.M. McCauley. Technical Report UMCS-92-12-2, Department of Computer Science, University of Manchester, 1992. (PostScript format.)

• Bibliography of papers in the Formal Aspects of Computing journal (also available as an unsorted version). (PostScript format.) BibTeX source also available.

• A list of Z books from the monthly Z FAQ message.

• Z bibliography.

• VDM text books.

• The VDM Bibliography, Peter Gorm Larsen. The BibTeX source also available. Second sourced including BibTeX format.

• Classified Larch Bibliography, S.J. Garland. LaTeX and BibTeX source also available.

• LaTeX reference list for the book Algebraic System Specification and Development: A Survey and Annotated Bibliography, edited by M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas and D. Sannella, Springer-Verlag, LNCS 501, 1991.

• Searchable safety-critical systems bibliography including many papers relevant to formal methods.

• CSP bibliography.

• ESPRIT ProCoS II project searchable bibliography.

• Formal methods subject area in the human computer interaction archive and the automated reasoning/deduction subject area in the theorem proving archive in the SEL-HPC Article Archive.

• FME Bibliographies links.

• Bibliography of works on Z and B (in French). .

Collections of on-line Technical Reports and papers

• Technical Monographs and Technical Reports from the Oxford University Computing Laboratory (OUCL). See also search facilities.

• Technical Reports from the University of Cambridge Computer Laboratory, UK. See also the Automated Reasoning Group including papers on HOL and Isabelle.

• Technical Reports from Department of Computer Science, University of Manchester, UK, including a list of reports and order form.

• Theory and Formal Methods Section of the Department of Computing, Imperial College of Science, Technology and Medicine, London, UK, including a research papers archive accessible by author (also by site).

• List of publications held at NASA Langley produced under NASA sponsorship since 1989 by various organizations. Some locally produced papers papers are available on-line.

• Technical Reports, DEC Systems Research Center, Palo Alto, California, USA (also via anonymous FTP including a README file, an index and abstracts).

• Reports and papers from SRI International Computer Science Laboratory, Menlo Park, California, USA, including a list of titles and abstracts. See also even more DVI files with abstracts and the NASA Langley list.

• SEI reports from the Software Engineering Institute, Carnegie-Mellon University, Pittsburgh, USA, including a large list of documents.

• CLI Technical Reports and FTP access at Computational Logic, Inc., Austin, Texas, USA. See also NASA Langley list.

• List of publications from ORA (Odyssey Research Associates), Ithaca, USA.

• SVCR publications from the Software Verification Research Centre, Dept. of Computer Science, The University of Queensland, Australia. See also departmental publications and Technical Reports via FTP.

• Formal methods in computer science journal titles and technical report abstracts.

• Selected publications from the Kestrel Institute, USA.

• Reports from the Laboratory for Foundations of Computer Science, University of Edinburgh, UK.

• Technical Reports from the Programming Methods Group, Computer Science Department, Åbo Akademi University, Finland.

• OPUS project papers on the formal foundations of object orientation, Programming Technology Lab, Department of Computer Science, Brussels Free University, Belgium.

• Annotated Bibliography of Recent Reports from ORA Canada.

• Technical Reports from the Hardware Verification Group at the University of Karlsruhe, Germany.

• Publications from the Center for High Assurance Computer Systems (CHACS), Information Technology Division, Naval Research Laboratory, Washington DC, USA.

If you are searching for on-line Technical Reports, you may find the Unified Computer Science Technical Report Index helpful. E.g., see a list of Technical Reports concerned with formal methods. See also a list of Computer Science Technical Reports archive sites.

Journals

• Acta Informatica.

• Annals of Software Engineering. (See also publisher information.)

• Applicable Algebra in Engineering, Communication and Computing.

• Australian Computer Journal. (See index.)

• Bulletin of the EATCS. See also basic information and EATCS Monographs.

• Communications of the ACM.

• The Computer Journal. On-line search facilities are available (e.g., see formal methods).

• Concurrency: Practice and Experience.

• Distributed Computing.

• electronic Workshops in Computing (eWiC). On-line international BCS journal covering computer science workshops, launched in July 1995.

• FACS Europe newsletter from BCS-FACS. Email FACS@lut.ac.uk.

• Formal Aspects of Computing. See also BCS information, subscription information, Manchester information and Madrid information. See also further pointers for published papers. Some information is available via anonymous FTP including a list of books on formal methods, a bibliography of papers in the journal (including an unsorted version) amongst other things.

• Formal Methods in System Design. The table of contents for journal issues is available.

• Journal of Automated Reasoning. See also here.

• Journal of University Computing. See Theory of Computation and other articles by category.

• IEE/BCS Software Engineering Journal. Ceased publication at the end of 1996. Relaunched as IEE Proceedings - Software.

• IEE Proceedings - Software (formerly IEE Proceedings - Software Engineering).

• Information and Software Technology journal. A Z special issue appeared in May/June 1995 (vol. 37, no. 5-6).

• Information Processing Letters.

• International Journal on Software Tools for Technology Transfer (STTT).

• Journal of the ACM.

• Journal of Formalized Mathematics.

• Journal of Software Maintenance: Research and Practice. See also here.

• Journal of Symbolic Computation.

• Journal of Systems and Software.

• Journal of Systems Architecture (formerly Microprocessing and Microprogramming). The EUROMICRO journal.

• Mathesis Universalis. A new electronic journal from Warsaw, Poland. Covers mechanized deduction, logic, etc.

• Microprocessors and Microsystems.

• Requirements Engineering.

• Science of Computer Programming.

• Software Engineering Notes newsletter from ACM SIGSOFT special interest group on Software Engineering.

• Software - Concepts and Tools.

• Software - Practice and Experience.

• Software Process - Improvement and Practice.

• Software Testing Verification & Reliability. See also here.

• Theoretical Computer Science from EATCS. (Also here from Elsevier).

• ACM Transactions on Programming Languages and Systems (TOPLAS).

• ACM Transactions on Software Engineering and Methodology (TOSEM).

• IEEE Transactions on Software Engineering. See Special Issue on Formal Methods in Software Practice, May 1997.

• ACM periodicals. See search for "formal methods" in ACM abstracts.

• Springer Journals in Computer Science.

• Computer science journals including reference information from the excellent Digital Bibliography & Library Project (DBLP) computer science bibliography. See also alternative ACM mirror site.

• The Directory of Computing Science Journals, a very comprehensive index. E.g., see under "Formal".

• Safety-related journals.

• LINK Alert Service for Springer computer science journals. Contents information sent by email as each issue is published.

Individual books

• Applications of Formal Methods, M.G. Hinchey and J.P. Bowen (eds.). Prentice Hall International Series in Computer Science, 1995. ISBN 0-13-366949-1.

• The B-Book: Assigning Programs to Meanings, J.-R. Abrial. Cambridge University Press, 1996. ISBN 0-521-49619-5.

• The B Language and Method: A Guide to Practical Formal Development, Kevin Lano. Springer-Verlag, FACIT series, May 1996. ISBN 3-540-76033-4.

• Case Studies in Systematic Software Development, C.B. Jones and R.C.F. Shaw (eds.). Prentice Hall International Series in Computer Science, 1990. ISBN 0-13-116088-5. (Out of print, ON-LINE BOOK!)

• Concurrent and Real-time Systems: The CSP Approach, S. Schneider. Wiley, 1999. ISBN 0-471-62373-3.

• FM'99 - Formal Methods, J.M. Wing, J. Woodcock and J. Davies. Springer-Verlag, LNCS 1708 (Volume I) and 1709 (Volume II), 1999. ISBN 3-540-66587-0 and 3-540-66588-9.

• FME'93: Industrial-Strength Formal Methods, J.C.P. Woodcock and P.G. Larsen. Springer-Verlag, LNCS 670, 1993. ISBN 3-540-56662-7.

• FME'94: Industrial Benefit of Formal Methods, M. Naftalin, T. Denvir and M. Bertran. Springer-Verlag, LNCS 873, 1994. ISBN 3-540-58555-9.

• FME'96: Industrial Benefits and Advances in Formal Methods, M.-C. Gaudel and J.C.P. Woodcock. Springer-Verlag, LNCS 1051, 1996. ISBN 3-540-60973-3.

• FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, J. Fitzgerald, C.B. Jones and P. Lucas. Springer-Verlag, LNCS 1313, 1997. ISBN 3-540-63533-5.

• Formal Description Techniques, IV, K.R. Parker. and G.A. Rose (eds.). IFIP Transactions C: Communication Systems, C-2, North-Holland, 1992. ISBN 0-444-89402-0.

• Formal Description Techniques, V, M. Diaz. and R. Groz (eds.). IFIP Transactions C: Communication Systems, C-10, North-Holland, 1993. ISBN 0-444-89282-6.

• Formal Description Techniques, VI, R.L. Tenney, P.D. Amer and M.Ü. Uyar (eds.). IFIP Transactions C: Communication Systems, C-22, North-Holland, 1994. ISBN 0-444-81773-5.

• Formal Development of Reactive Systems: Case Study Production Cell, C. Lewerentz and T. Lindner. Springer-Verlag, LNCS 891, 1995. ISBN 3-540-58867-1.

• Formal Hardware Verification: Methods and Systems in Comparison, T. Kropf (ed.). Springer-Verlag, LNCS 1287, 1997. ISBN 3-540-63475-4.
• Formal Methods for Interactive Systems, Alan Dix. Academic Press, 1991. ISBN 0-12-218315-0.

• Formal Methods for Real-Time Computing, C. Heitmeyer and D. Mandrioli (eds.). Trends in Software series, volume 5, John Wiley & Sons, 1996. ISBN 0-471-95835-2.

• Formal Specification and Documentation using Z, J.P. Bowen. International Thomson Computer Press, 1996. ISBN 1-850-32230-9.

• Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever and J. Vytopil. Springer-Verlag, LNCS 863, 1994. ISBN 3-540-58468-4.

• High-Integrity System Specification and Design, M.G. Hinchey and J.P. Bowen. FACIT series, Springer-Verlag, London, 1999. ISBN 3-540-76226-4.

• Industrial-Strength Formal Methods in Practice, M.G. Hinchey and J.P. Bowen (eds.). FACIT series, Springer-Verlag, London. ISBN 1-85233-640-4. In preparation, to appear 1999.

• Modelling Systems: Practical Tools and Techniques for Software Development, J. Fitzgerald and P.G. Larsen. Cambridge University Press, 1998. ISBN 0521623480 (paperback) & 0521626056 (hardback).

• Notations for Software Design, L.M.G. Feijs, H.B.M. Jonker and C.A. Middelburg. Springer-Verlag, 1994. ISBN 3-540-19902-0.

• Programming Concepts, Methods and Calculi, E.-R. Olderog (ed.). IFIP Transactions A: Computer Science and Technology, A-56, North-Holland, 1994. ISBN 0-444-82020-5.

• Programming from Specifications, 2nd edition, C.C. Morgan. Prentice Hall International Series in Computer Science, 1994. ISBN 0-13-123274-6.

• Proof, Language, and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M. Tofte (eds.). The MIT Press, 2000. ISBN 0-262-16188-5.

• Protocol Specification, Testing and Verification, XII, J. Linn, Jr. and M.Ü. Uyar. IFIP Transactions C: Communication Systems, C-8, North-Holland, 1992. ISBN 0-444-89874-3.

• Protocol Specification, Testing and Verification, XIII, A. Danthine., G. Leduc. and P. Wolper (eds.). IFIP Transactions C: Communication Systems, C-16, North-Holland, 1993. ISBN 0-444-81648-8.

• Semantics with Applications: A Formal Introduction, H.R. Nielson and F. Nielson. Wiley Professional Computing, 1992. ISBN 0-471-92980-8. Revised gzipped PostScript version available, July 1999.

• The Steam Boiler Control Specification Problem, J.-R. Abrial, E. Börger and H. Langmaack. Springer-Verlag, LNCS 1165, 1996. ISBN 3-540-61929-1.

• Systematic Software Development Using VDM, 2nd edition, C.B. Jones. Prentice Hall International Series in Computer Science, 1991. ISBN 0-13-880733-7. See also teachers notes. (Out of print, ON-LINE BOOK!)

• The Theory and Practice of Concurrency, A.W. Roscoe. Prentice Hall International Series in Computer Science, 1997. ISBN 0-13-674409-5.

• Towards Verified Systems, J.P. Bowen (ed.). Real-Time Safety Critical Systems series, volume 2, Elsevier, 1994. ISBN 0-444-89901-4.

• Using Z: Specification, Refinement and Proof, J. Davies and J.C.P. Woodcock. Prentice Hall International Series in Computer Science, 1996. 1996. ISBN 0-13-948472-8.

• Z User Workshop, London 1992, J.P. Bowen and J.E. Nicholls (eds.). Springer-Verlag, Workshops in Computing, 1993. ISBN 3-540-19818-0.

• Z User Workshop, Cambridge 1994, J.P. Bowen and J.A. Hall (eds.). Springer-Verlag, Workshops in Computing, 1994. ISBN 3-540-19884-9.

• ZUM'95: The Z Formal Specification Notation, J.P. Bowen and M.G. Hinchey (eds.). Springer-Verlag, LNCS 967, 1995. ISBN 3-540-60271-2.

• ZUM'97: The Z Formal Specification Notation, J.P. Bowen, M.G. Hinchey and D. Till. Springer-Verlag, LNCS 1212, 1997. ISBN 3-540-62717-0.

• ZUM'98: The Z Formal Specification Notation, J.P. Bowen, A. Fett and M.G. Hinchey. Springer-Verlag, LNCS 1493, 1998. ISBN 3-540-65070-9.

See also:

• Formal methods books listed by Amazon. See also UK site.

• Z User Meeting proceedings.

• Lecture Notes in Computer Science (LNCS), Springer-Verlag, Berlin.

• Books on Program Verification And Reliability and Requirements/Specifications from Prentice Hall.

• Prentice Hall International Series in Computer Science, including many books on formal methods.

• Formal Approaches to Computing and Information Technology series (FACIT), Springer-Verlag, London.

• Formal Methods Guide Books information from FME.

Selected Technical Reports and on-line papers

• Safety-Critical Systems, Formal Methods and Standards, J.P. Bowen and V. Stavridou. IEE/BCS Software Engineering Journal, 8(4):189-209, July 1993. Previously available as Oxford University Computing Laboratory Technical Report PRG-TR-5-92, 1992. See also Chapter 1 in Towards Verified Systems. Winner of the IEE Charles Babbage Premium award, 1994.

• The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective, J.P. Bowen and V. Stavridou. In J.C.P. Woodcock and P.G. Larsen (eds.), FME'93: Industrial-Strength Formal Methods, Springer-Verlag, LNCS 670, pp 183-195, 1993.

• Seven More Myths of Formal Methods, J.P. Bowen and M.G. Hinchey. University of Cambridge Computer Laboratory Technical Report 357, 12pp, January 1995. Revised version in IEEE Software, 12(4):34-41, July 1995.

• An International Survey of Industrial Applications of Formal Methods, D. Craigen, S. Gerhart and T.J. Ralston, 1993.
  • Volume 1: Purpose, Approach, Analysis and Conclusions.
  • Volume 2: Case Studies.

• Specifications are not (necessarily) executable, I.J. Hayes and C.B. Jones. Technical Report UMCS-89-12-1, Department of Computer Science, University of Manchester, 1989. Also published in IEE/BCS Software Engineering Journal, 4(6):320-338, November 1989.

• Understanding the differences between VDM and Z, I.J. Hayes, C.B. Jones and J.E. Nicholls. Technical Report UMCS-93-8-1, Department of Computer Science, University of Manchester, 1993.

• Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods, S.P. Miller and M. Srivas. To be presented at WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, April 5-8, 1995, Boca Raton, Florida USA.

• Formal Methods Specification and Verification Guidebook for Software and Computer Systems, NASA JPL, Pasadena, CA, USA.
  • Volume I: Planning and Technology Insertion, [NASA-GB-002-95], 1995, 77 pages.
  • Volume II: A Practitioner's Companion, [NASA-GB-001-97], 1997, 245 pages.

• Formal Methods for the Specification and Design of Real-Time Safety Critical Systems, J. Ostroff. Journal of Systems and Software, 18(1):33-60, April 1992.

• Formal Methods and their Role in the Certification of Critical Systems, J. Rushby. SRI Technical Report CSL-95-1, March 1995.
  This is a shorter (50 pages) and less technical treatment of the material in CSL-93-7 (300 pages). It will become a chapter in the FAA Digital Systems Validation Handbook (a guide to assist FAA Certification Specialists with advanced technology issues).

• A survey of formal software development methods, D. Sannella, 1988. Appeared in Software Engineering: A European Prospective, A. McGettrick and R. Thayer (eds.), IEEE Computer Society Press, pp 281-297, 1993.

• Formal program development in Extended ML for the working programmer, D. Sannella. Appeared in Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park, Springer, Workshops in Computing, pp 99-130, 1991.

• Formal methods and their role in developing safe systems, Muffy Thomas. IEE Workshop report, 20 March 1995.

Part of the OUCL archive.