40 Years of Formal Methods Some obstacles and some possibilities

Dines Bjorner Prof. Emeritus, Technical University of Denmark)

In this "40 years of formal methods" essay we shall first delineate 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 we shall provide a "survey": which are the `prerequisite works' that have enabled formal methods; and which are, to us, the, by now, classical `formal methods'. We then ask ourselves the question: Have formal methods for software development, in the sense of this talk been successful? Our answer is, regretfully, no! We motivate this answer 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 by a "looking forward" at some promising developments besides the alleviation of the (eighth or more) hindrances!

Please see : https://www.jaist.ac.jp/rcsv/event/20140418-eventsmr/kanazawa-s.pdf for slides.