Publications

Virtual Library

---

Computing

---

Software engineering

---

Formal methods

This document contains some pointers to publications concerning formal methods, especially those that are online, which are available on the World Wide Web.

Introduction

For a good general introduction to formal methods, see:

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

Another excellent introduction to some of the issues concerned with formal methods is:

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

The September 1990 issues of Computer, IEEE Software and IEEE Transactions on Software Engineering all contained articles on formal methods. A follow-up article as also available:

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

The above three papers are reprinted in the book High-Integrity System Specification and Design, 1999.

For some guidance on the industrial use of formal methods, see:

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

For an update ten years later, see:

J.P. Bowen and M.G. Hinchey, Ten Commandments of Formal Methods ... Ten Years Later. IEEE Computer, 39(1):40-48, January 2006.

See also earlier conference version:

Ten Commandments Revisited: A Ten-Year Perspective on the Industrial Application of Formal Methods. In T. Margaria and M. Massink (eds.), FMICS 05: Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, Portugal, 5–6 September 2005, pages 8-16. ACM, 2005.

A roundtable discussion on formal methods by some "noted experts" may be found in:

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

For a comparison of using formal methods versus not using formal methods, see:

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

See the group report from the Strategic Directions in Computing Research Formal Methods Working Group ACM Workshop, USA, August 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.)
Published in: ACM Computing Surveys, 28(4):626-643, 1996.

Finally, some more general articles setting formal methods in context:

Building a Better Bug-trap, The Economist, Science Technology Quarterly, 19 June 2003.Richard Sharpe, Formal Methods Start to Add up Again, Computing, 8 January 2004.Philip E. Ross, The Exterminators, IEEE Spectrum, pages 36–41, September 2005.

See also Formal Methods papers links from Roger Pressman.

Bibliographies

The following online information is available:

• Bibliographies on Software/Hardware Engineering and Formal Methods from a large Collection of Computer Science Bibliographies. Search for "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, and Z notation 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.
• 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.
• Safety-critical systems bibliography including many papers relevant to formal methods.
• ESPRIT ProCoS II project bibliography.
• Bibliography of works on Z and B (in French).
• Formal methods publications from Google Scholar.
• Formal methods books from Google Book Search.

Collections of online Technical Reports and papers

The following sites have produced online Reports including some on Formal Methods which may be of interest:

• Technical Monographs and Technical Reports from the Oxford University Computing Laboratory (OUCL).
• 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 are available online.
• Technical Reports, Compaq Systems Research Center, Palo Alto, California, USA.
• Publications from SRI International Computer Science Laboratory, Menlo Park, California, USA.
• List of SEI Reports from the Software Engineering Institute, Carnegie-Mellon University, Pittsburgh, USA.
• CLI Technical Reports and FTP access at Computational Logic, Inc., Austin, Texas, USA.
• SVCR Publications Archive from the Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland, Australia. See also School Research Reports, especially Software Engineering.
• Selected publications from the Kestrel Institute, USA.
• Research Publications from the Laboratory for Foundations of Computer Science, University of Edinburgh, UK.
• Bibliography from ORA Canada, Ottawa, Canada.
• Publications from the Formal Methods Group, University of Karlsruhe, Germany.
• Publications from the Center for High Assurance Computer Systems (CHACS), Information Technology Division, Naval Research Laboratory, Washington DC, USA.
• World Congress on Formal Methods (FM), Z Users Conference (ZUM) and other Computer Science Conferences & Workshops publications from DBLP.

If you are searching for online 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

The following journals are either exclusively devoted to formal methods or include papers appertaining to formal methods including the underlying theory and software engineering aspects:

• 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. (European Association for Theoretical Computer Science.) See also EATCS publications.
• 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 British Computer Society (BCS) series covering computer science workshops including formal methods and formal aspects, launched in July 1995.
• FACS FACTS newsletter from BCS-FACS.
• 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) among other things.
• Formal Methods in System Design. The table of contents for journal issues is available.
• Formal Methods Letters (FML), a special section in the STTT journal.
• International Journal on Software Tools for Technology Transfer (STTT). Includes a Formal Methods Letters (FML) section.
• Journal of Automated Reasoning. See also here.
• IEE/BCSSoftware Engineering Journal. Ceased publication at the end of 1996. Relaunched as IEE Proceedings - Software.
• IEE Proceedings - Software (formerly IEE Proceedings - Software Engineering). Published by IET since 2006.
• 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 Computational Logic (TOCL).
• ACM Transactions on Programming Languages and Systems (TOPLAS).
• ACMTransactions on Software Engineering and Methodology (TOSEM).
• IEEETransactions on Software Engineering. See Special Issue on Formal Methods in Software Practice, May 1997.

See also:

• ACM periodicals.
• 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

The following books have online information associated with them:

• Abstract State Machines: A Method for High-Level System Design and Analysis, Egon Börger and Robert Stärk. Springer-Verlag, 2003. ISBN 3-540-00702-4.
• 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 (eds.). Springer-Verlag, LNCS 1708 (Volume I) and 1709 (Volume II), 1999. ISBN 3-540-66587-0, ISBN 3-540-66588-9.
• FME'93: Industrial-Strength Formal Methods, J.C.P. Woodcock and P.G. Larsen (eds.). Springer-Verlag, LNCS 670, 1993. ISBN 3-540-56662-7.
• FME'94: Industrial Benefit of Formal Methods, M. Naftalin, T. Denvir and M. Bertran (eds.). 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 (eds.). 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.
• FME 2001: Formal Methods for Increasing Software Productivity, J.N. Oliveira and P. Zave (eds.). Springer-Verlag, LNCS 2021, 2001. ISBN 3-540-41791-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, [Jonathan Bowen|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, 1999. ISBN 1-85233-640-4.
• Java and the Java Virtual Machine: Definition, Verification, Validation, R. St�rk, J. Schmid and E. Börger. Springer-Verlag, 2001. With CD-ROM. ISBN 3-540-42088-6.
• Modelling Systems: Practical Tools and Techniques for Software Development, J. Fitzgerald and P.G. Larsen. Cambridge University Press, 1998. ISBN 0521623480 (paperback) & ISBN 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.
• Practical Theory of Programming, E.C.R. Hehner. Springer-Verlag, 1993. ISBN 0387941061.
• 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.
• Refinement in Z and Object-Z: Foundations and Advanced Applications, John Derrick and Eerke Boiten. FACIT series, Springer-Verlag, London, 2001. ISBN 1-85233-245-X.
• 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.
• Software Specification Methods: An Overview Using a Case Study, M. Frappier and H. Habrias (eds.). FACIT series, Springer-Verlag, London, 2001. ISBN 1-85233-640-4. Publisher information.
• The Steam Boiler Control Specification Problem, J.-R. Abrial, E. Börger and H. Langmaack (eds.). 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.
• A Unifying Framework for Structured Analysis and Design Models: an Approach using Initial Algebra Semantics and Category Theory, T.H. Tse. Cambridge Tracts in Theoretical Computer Science, vol. 11, Cambridge University Press. Hardback edition, 1991. ISBN 9780521391962. Paperback edition, 2009. ISBN 9780521117876.
• Using Z: Specification, Refinement and Proof, J. Davies and J.C.P. Woodcock. Prentice Hall International Series in Computer Science, 1996. ISBN 0-13-948472-8.
• ZB2000: Formal Specification and Development in Z and B, 1st International Conference of B and Z Users, York, UK, 29 August – 2 September 2000, Jonathan P. Bowen, Steve Dunne, Andy Galloway and Steve King (eds.). Springer-Verlag, LNCS1878, August 2000. ISBN 3-540-67944-8.
• ZB2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, France, 23-25 January 2002, Didier Bert, Jonathan P. Bowen, Martin Henson and Ken Robinson (eds.). Springer-Verlag, LNCS 2272, January 2002. ISBN 3-540-43166-7.
• 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, LNCS1212, 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.
• 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 books available online from FreeTechBooks.com.

Selected Technical Reports and online papers

The following are deemed to be of general interest:

• 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.
• 6th International Workshop on Formal Methods, Joseph M. Morris, Benjamin Aziz and Frédéric Oehl (eds.), BCS Electronic Workshops in Computing (eWiC), Dublin City University, Ireland, 11 July 2003.

See the most cited computer science authors (many related to formal methods) in the CiteSeer database. See also the most cited computer science articles and the most cited computer science publications.

Formal methods search for papers under Z User Conference papers from DoCIS.

---

Last updated by Jonathan Bowen, 1 April 2009.
Further information for possible inclusion is welcome.