Virtual Library

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 some guidance on the industrial use of formal methods, see:

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

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

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.

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.)
Published in: ACM Computing Surveys, 28(4):626-643, 1996.

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.

Phipip E. Ross, The Exterminators, IEEE Spectrum, pages 36-41, September 2005.

See also Formal Methods papers links from Roger Pressman.

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.

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

• ESPRIT ProCoS II project searchable bibliography.

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

• Formal methods puplications from Google Scholar.

• Formal methods books from Google Print. .

Collections of online Technical Reports and papers

• 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

• 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/BCS Software 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).

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

• 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

• 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 and 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, 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) & 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.

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

• 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, LNCS 1878, 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, 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.

• 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

• 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 most cited authors in computer science (many related to formal methods) in the Research Index database. See also top 10,000 cites authors in Computer Science.

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

Part of the LSBU Museophile archive.