40 years of formal methods

Dines Bjørner, Klaus Havelund

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


In this "40 years of formal methods" essay we shall first delineate, Sect. 1, what we mean by method, formal method, computer science, computing science, software engineering, and model-oriented and algebraic methods. Based on this, we shall characterize a spectrum from specification-oriented methods to analysis-oriented methods. Then, Sect. 2, we shall provide a "survey": which are the 'prerequisite works' that have enabled formal methods, Sect. 2.1, and which are, to us, the, by now, classical 'formal methods', Sect. 2.2. We then ask ourselves the question: have formal methods for software development, in the sense of this paper been successful? Our answer is, regretfully, no! We motivate this answer, in Sect. 3.2, by discussing eight obstacles or hindrances to the proper integration of formal methods in university research and education as well as in industry practice. This "looking back" is complemented, in Sect. 3.4, by a "looking forward" at some promising developments-besides the alleviation of the (eighth or more) hindrances! © 2014 Springer International Publishing Switzerland.
Original languageEnglish
Title of host publicationFM 2014: Formal Methods : Proceedings of 19th International Symposium
Number of pages20
Publication date2014
ISBN (Print)978-3-319-06409-3
ISBN (Electronic) 978-3-319-06410-9
Publication statusPublished - 2014
Event19th International Symposium on Formal Methods - Singapore, Singapore
Duration: 12 May 201416 May 2014
Conference number: 19


Conference19th International Symposium on Formal Methods
SeriesLecture Notes in Computer Science


  • Computer Science (all)
  • Theoretical Computer Science
  • Algebra
  • Algebraic method
  • Computing science
  • Industry practices
  • University research
  • Formal methods

Fingerprint Dive into the research topics of '40 years of formal methods'. Together they form a unique fingerprint.

Cite this