Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Origins and Development of Formal Methods

  • Chapter
  • First Online:
Formal Methods for Software Engineering

Part of the book series: Texts in Theoretical Computer Science. An EATCS Series ((TTCS))

Abstract

This chapter offers an historical perspective on the development of Formal Methods for software engineering. It surveys some of the problems and solution methods that have shaped and become our theoretical understanding and practical capability for making software. Starting in the 1950s, the history is organised by the topics of programming, data, reasoning, and concurrency, and concludes with a selection of notes on application areas relevant to the book. Although the account emphasizes some contributions and neglects others, it provides a starting point for studying the development of the challenging and ongoing enterprise that is software engineering.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 84.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Change history

  • 20 December 2022

    .

Notes

  1. 1.

    An account of the conference and copies of the proceedings are available at http://homepages.cs.ncl.ac.uk/brian.randell/NATO.

  2. 2.

    By 1954 the cost of programming was becoming comparable with the cost of computer installations, which was a prime motivation for IBM’s development of Fortran [Bac98].

  3. 3.

    The following decade saw a rich harvest of textbooks on processing syntax, six by Ullman, Hopcroft and Aho.

  4. 4.

    Imperative programming has at its heart a language containing only assignments, sequencing, conditional branching and conditional iteration.

  5. 5.

    Along with suggestions about encapsulation, polymorphism, static type checking and exception handling!

  6. 6.

    Just as studies of recursive definitions of higher types in programming languages led to the semantic framework of domain theory.

  7. 7.

    Along with Defence Standard 00-55 there was an umbrella standard for identifying and reducing risks and so to determine when 00-55 would apply. The standards have been revised several times subsequently and the explicit requirement for Formal Methods has been removed.

References

  1. Krzysztof Apt, Frank S de Boer and Ernst-Rüdiger Olderog,Verification of Sequential and Concurrent Programs, Springer, 2009.

    Google Scholar 

  2. Frances E. Allen, The history of language processor technology in IBM, IBM Journal of Research and Development, 25 (5) (1981), 535–548.

    Google Scholar 

  3. Krzysztof Apt and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs, Springer, 1991.

    Google Scholar 

  4. Krzysztof Apt, Ten years of Hoare’s logic: A survey – Part I, ACM Transactions on Programming Languages and Systems, 3 (4) (1981), 431–483.

    MATH  Google Scholar 

  5. Krzysztof Apt, Ten years of Hoare’s logic: A survey – Part II: Nondeterminism, Theoretical Computer Science, 28 (1-2) 1983, 83–109.

    MathSciNet  MATH  Google Scholar 

  6. Jean-Raymond Abrial, Stephen A Schuman, and Bertrand Meyer, A specification language, in A M Macnaghten and R M McKeag (editors), On the Construction of Programs, Cambridge University Press, 1980.

    Google Scholar 

  7. Ralph-Johan Back, Correctness Preserving Program Refinements: Proof Theory and Applications, Mathematical Centre Tracts 131, Mathematical Centre, Amsterdam, 1980.

    Google Scholar 

  8. John Backus, The history of Fortran I, II, and III, IEEE Annals of the History of Computing, 20 (1998) (4), 68–78.

    Google Scholar 

  9. Jos C.M. Baeten, A brief history of process algebra, Theoretical Computer Science, 335 (2-3) (2005), 131–146.

    MathSciNet  Google Scholar 

  10. Jaco de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall International Series in Computer Science, 1980.

    Google Scholar 

  11. Jos C.M. Baeten and Jan A. Bergstra, Discrete time process algebra, Formal Aspects of Computing, 8 (1996) (2), 188–208.

    Google Scholar 

  12. Jos C M Baeten, T. Basten, and M.A. Reniers, Process Algebra: Equational Theories of Communicating Processes, Cambridge Tracts in Theoretical Computer Science 50, Cambridge University Press, 2010.

    Google Scholar 

  13. Jos C M Baeten, Jan A Bergstra, and Scott A. Smolka, Axiomatising probabilistic processes: ACP with generative probabilities, in CONCUR 92, Lecture Notes in Computer Science 630, Springer, 1992, 472–485.

    Google Scholar 

  14. Jos C M Baeten, Jan A Bergstra, and Scott A. Smolka, Axiomatizing probabilistic processes: ACP with generative probabilities, Information and Computation, 121(1995) (2), 234–254.

    Google Scholar 

  15. Yves Bertot and Pierre Castéran, Interactive Theorem Proving and Program Development. Coq art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science: an EATCS series, Springer, 2004.

    Google Scholar 

  16. L. Bouge, N.Choquet, L. Fribourg, and M.-C. Gaudel. Test set generation from algebraic specifications using logic programming. Journal of Systems and Software, 6 (4) (1986) 343–360.

    Google Scholar 

  17. Manfred Broy and Ernst Denert (editors), Software Pioneers: Contributions to Software Engineering, Springer-Verlag, 2002.

    Google Scholar 

  18. Ana Bove, Peter Dybjer and Ulf Norell, A Brief Overview of Agda – A Functional Language with Dependent Types, in Stefan Berghofer, Tobias Nipkow, Christian Urban and Makarius Wenzel (editors), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5674, Springer-Verlag, 2009, 73–78.

    Google Scholar 

  19. Hans Bekić, Towards a mathematical theory of processes, Technical Report TR 25.125, IBM Laboratory Vienna, 1971. Reprinted in [BJ84].

    Google Scholar 

  20. D. Elliott Bell, Looking back at the Bell-La Padula model, ACSAC ’05 Proceedings of the 21st Annual Computer Security Applications Conference, IEEE Computer Society, 2005, 337–351.

    Google Scholar 

  21. Rod Burstall and Joseph Goguen. The semantics of Clear, a specification language. In Dines Bjørner (editor), Abstract Software Specification – 1979 Copenhagen Winter School, Lecture Notes in Computer Science 86, Springer, 1980, 292–332.

    Google Scholar 

  22. Dines Bjørner, Anne Elisabeth Haxthausen, Klaus Havelund, Formal, model-oriented software development methods: From VDM to ProCoS and from RAISE to LaCoS, Future Generation Computer Systems 7 (2-3) (1992), 111–138.

    Google Scholar 

  23. Anya Helene Bagge and Magne Haveraaen, Specification of generic APIs, or: why algebraic may be better than pre/post, in High integrity language technology 2014, ACM, 2014, 71–80.

    Google Scholar 

  24. Jan A Bergstra, Jan Heering, and Paul Klint (editors), Algebraic Specification, ACM Press/Addison-Wesley, 1989.

    Google Scholar 

  25. Dines Bjørner and Cliff Jones, Formal Specification and Software Development, Prentice Hall International, 1982.

    Google Scholar 

  26. Hans Bekić and Cliff Jones (editors), Programming Languages and Their Definition: H. Bekić (1936–1982), Lecture Notes in Computer Science 177, Springer, 1984.

    Google Scholar 

  27. Grady Booch, Ivar Jacobson and James Rumbaugh, The Unified Modeling Language for Object-Oriented Development Documentation Set Version 0.91. Addendum UML Update, Rational Software Corporation, 1996.

    Google Scholar 

  28. Jan A Bergstra and Jan Willem Klop, Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Centre, Amsterdam, 1982.

    Google Scholar 

  29. Jan A Bergstra and Jan Willem Klop, Process algebra for synchronous communication. Information and Control 60 (1-3) (1984), 109–137.

    Google Scholar 

  30. Robert S.Boyer, Matt Kaufmann, Joseph S Moore, The Boyer-Moore theorem prover and its interactive enhancement, Computers and Mathematics with Applications, 29 (2) (1995), 27–62.

    MathSciNet  Google Scholar 

  31. D. Elliott Bell and Leonard J. LaPadula, Secure computer systems: Vol. I mathematical foundations, Vol. II mathematical model, Vol III refinement of the mathematical model. Technical Report MTR-2547 (three volumes), Mitre Corporation, Bedford, MA, 1973.

    Google Scholar 

  32. D. Elliott Bell and Leonard J. LaPadula, Secure computer system: Unified exposition and Multics interpretation. Technical Report ESD-TR-75-306, Mitre Corporation, Bedford, MA, 1976.

    Google Scholar 

  33. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte, The Spec# programming system: an overview, in Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean (editors), Construction and Analysis of Safe, Secure and Interoperable Smart Devices, Lecture Notes in Computer Science 3362, Springer-Verlag, 2005, 49–69.

    Google Scholar 

  34. Jan A Bergstra, Alban Ponse and Scott A Smolka, Handbook of Process Algebra, Elsevier 2001.

    Google Scholar 

  35. Jaco de Bakker and Jan Rutten (editors), Ten Years of Concurrency Semantics. Selected Papers of the Amsterdam Concurrency Group, World Scientific, 1992.

    Google Scholar 

  36. Fred Brooks, The Mythical Man-Month: Essays on Software Engineering, Addison Wesley, 1975. Republished 1995.

    Google Scholar 

  37. Fred Brooks, No Silver Bullet – Essence and Accidents of Software Engineering, IEEE Computer, 20 (1987) (4), 10–19.

    MathSciNet  Google Scholar 

  38. Jan A Bergstra and John V Tucker, The completeness of the algebraic specification methods for data types, Information and Control, 54 (1982), 186–200.

    Google Scholar 

  39. Jan A Bergstra and John V Tucker, Expressiveness and the completeness of Hoare’s logic, Journal of Computer and System Sciences, 25 (3) (1982), 267–284.

    Google Scholar 

  40. J A Bergstra and John V Tucker, The axiomatic semantics of programs based on Hoare’s logic, Acta Informatica, 21 (1984), 293–320.

    Google Scholar 

  41. J A Bergstra and John V Tucker, Hoare’s logic for programming languages with two data types, Theoretical Computer Science, 28 (1984) 215–221.

    Google Scholar 

  42. Jan A Bergstra and John V Tucker, Algebraic specifications of computable and semicomputable data types, Theoretical Computer Science, 50 (1987), 137–181.

    Google Scholar 

  43. Jan A Bergstra and John V Tucker, Equational specifications, complete term rewriting systems, and computable and semicomputable algebras, Journal of ACM, 42 (1995), 1194–1230.

    Google Scholar 

  44. Jan A Bergstra and John V Tucker, The rational numbers as an abstract data type, Journal of the ACM, 54 (2), (2007), Article 7.

    Google Scholar 

  45. Rod BurstalI, Program proving as hand simulation with a little induction, in Information Processing ’74, 308-312. North-Holland, 1974.

    Google Scholar 

  46. Peter Burmeister, A Model Theoretic Oriented Approach to Partial Algebras, Akademie-Verlag, 1986.

    Google Scholar 

  47. Jos C.M. Baeten and W. Weijland. Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

    Google Scholar 

  48. Jaco de Bakker and Jeffrey I Zucker, Processes and the denotational semantics of concurrency, Information and Control, 54 (1/2) (1982), 70–120.

    Google Scholar 

  49. Martin Campbell-Kelly, From Airline Reservations to Sonic the Hedgehog: A History of the Software Industry, MIT Press, 2003.

    Google Scholar 

  50. James L Caldwell, Formal methods technology transfer: A view from NASA, Formal Methods in System Design, 12 (1998), 125–137.

    Google Scholar 

  51. Edmund M Clarke and E Allen Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, in Dexter Kozen (editor), Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.

    Google Scholar 

  52. Stuart K Card, William K. English and Betty J Burr, Evaluation of mouse, rate-controlled isometric joystick, step keys and text keys on a CRT, Ergonomics, 21:8 (1977) 601–613.

    Google Scholar 

  53. Noam Chomsky, Three models for the description of language, IRE Transactions on Information Theory, 2 (1956), 113–124.

    MATH  Google Scholar 

  54. Noam Chomsky, and G. A. Miller, Finite state languages, Information and Control, 1 (1958), 91–112.

    Google Scholar 

  55. Noam Chomsky, On certain formal properties of grammars, Information and Control, 2 (1959), 137–167.

    MathSciNet  MATH  Google Scholar 

  56. Edmund M. Clarke, The birth of model checking, in Orna Grumberg and Helmut Veith (editors), 25 Years of Model Checking: History, Achievements, Perspectives, Lecture Notes in Computer Science 5000, Springer-Verlag, 1–26, 2008.

    Google Scholar 

  57. Stuart K. Card, Thomas P. Moran, Allen Newell, The Psychology of Human-Computer Interaction, L. Erlbaum Associates, 1983.

    Google Scholar 

  58. Robert L Constable, Implementing Mathematics with the NUPRL Proof Development System, Prentice Hall, 1986.

    Google Scholar 

  59. Robert L Constable, The triumph of types: Principia Mathematica’s impact on computer science, Unpublished: available, e.g., at https://sefm-book.github.io.

  60. David Cooper, Programs for mechanical program verification, in B. Melzer and D. Michie, editors, Machine Intelligence 6, Edinburgh University Press, 1971, 43–59.

    Google Scholar 

  61. David Cooper, Theorem proving in arithmetic without multiplication, in B. Melzer and D. Michie (editors), Machine Intelligence 7, Edinburgh University Press, 1972, 91–99.

    Google Scholar 

  62. Stephen A Cook, Soundness and completeness of an axiom system for program verification. SIAM J. Computing 7 (1) (1978), 70–90.

    Google Scholar 

  63. Pierre-Louis Curien. Symmetry and interactivity in programming. Bulletin of Symbolic Logic, 9: 2 (2003), 169–180.

    MathSciNet  MATH  Google Scholar 

  64. Edmund M Clarke and Jeannette Wing, Formal methods: state of the art and future directions, ACM Computing Surveys, 28 (4) (1996), 626–643.

    Google Scholar 

  65. Edgar Daylight, The Dawn of Software Engineering: From Turing to Dijkstra, Lonely Scholar, 2012.

    Google Scholar 

  66. Dorothy Denning, A lattice model of secure information flow, Communications of the ACM 19 (5) (1976) , 236–243.

    MathSciNet  MATH  Google Scholar 

  67. Dorothy Denning and Peter Denning, Certification of programs for secure information flow,Communications of the ACM, 20 (7) (1977) , 504–513.

    MATH  Google Scholar 

  68. Stéphane Demi, Valentin Goranko and Martin Lange, Temporal Logics in Computer Science and Finite State Systems, Cambridge Tracts in Theoretical Computer Science 58, Cambridge UP, 2016.

    Google Scholar 

  69. Răzvan Diaconescu, Three decades of institution theory, in Jean-Yves Béziau (editor), Universal Logic: An Anthology, Springer Basel, 2012, 309–322.

    Google Scholar 

  70. Edsger W Dijkstra, Over de sequentialiteit van procesbeschrijvingen, E.W. Dijkstra Archive. Center for American History, University of Texas at Austin, undated, 1962 or 1963.

    Google Scholar 

  71. Edsger W Dijkstra, Cooperating sequential processes, in F. Genuys (editor) Programming Languages, 1968, Academic Press, 43–112.

    Google Scholar 

  72. Edsger W Dijkstra, The structure of the THE multiprogramming system, Communications of the ACM, 11 (5) (1968), 341–346.

    Google Scholar 

  73. Edsger W Dijkstra, Go to statement considered harmful, Communications of the ACM, 11 (3) (1968), 147–148.

    Google Scholar 

  74. Edsger W Dijkstra, The humble programmer, Communications of the ACM, 11 (10) (1972), 859–866.

    Google Scholar 

  75. Edsger W Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.

    Google Scholar 

  76. Edsger W Dijkstra, Selected Writings on Computing: A Personal Perspective. Springer-Verlag, 1982.

    Google Scholar 

  77. Alan J Dix, Formal Methods and Interactive Systems: Principles And Practice, D.Phil. Thesis, Department of Computer Science, University of York, 1987.

    Google Scholar 

  78. Alan J Dix, Formal Methods for Interactive Systems, Cambridge UP, 1991.

    Google Scholar 

  79. Alan J Dix and M D Harrison, Principles and interaction models for window managers, in M D Harrison A F Monk (editors) People and computers: designing for usability, Cambridge UP, 1986, 352–366.

    Google Scholar 

  80. Alan J Dix and Colin Runciman, Abstract models of interactive systems, P J and S Cook (editors), People and computers: designing the interface, Cambridge UP, 1985, 13–22.

    Google Scholar 

  81. B. Elspas, M. Green, M. Moriconi, and R. Shostak, A JOVIAL verifier. Technical report, Computer Science Laboratory, SRI International, January 1979.

    Google Scholar 

  82. E. Allen Emerson, The beginning of model checking: A personal perspective, in Orna Grumberg and Helmut Veith (editors), 25 Years of Model Checking: History, Achievements, Perspectives, Lecture Notes in Computer Science 5000, Springer-Verlag, 27–45, 2008.

    Google Scholar 

  83. Robert W Floyd, On the nonexistence of a phrase structure grammar for ALGOL 60. Communications of the ACM, 5 (9) (1962), 483–484.

    Google Scholar 

  84. Robert W Floyd, Assigning meanings to programs, in Jacob Schwartz (editor) Proceedings of Symposia in Applied Mathematics 19, American Mathematical Society, 1967, pp. 19–32.

    Google Scholar 

  85. Willem Jan Fokkink, Introduction to Process Algebra, Texts in Theoretical Computer Science, An EATCS Series. Springer, January 2000.

    Google Scholar 

  86. Leslie Fox (editor), Advances in Programming and Non-numerical Computation, Pergamon Press, 1966.

    Google Scholar 

  87. Marie-Claude Gaudel, Testing can be formal, too, in Peter D. Mosses, M. Nielsen and M. I. Schwartzbach, (editors), TAPSOFT, Lecture Notes in Computer Science 915, Springer-Verlag, 1995, 82–96.

    Google Scholar 

  88. Rob van Glabbeek, Comparative concurrency semantics and refinement of actions, CWI Tract 109, CWI Amsterdam, 1996.

    Google Scholar 

  89. John V Guttag and James J. Horning, The algebraic specification of abstract data types, Acta Informatica 10 (1) (1978) 27–52.

    Google Scholar 

  90. John V Guttag, James J. Horning, and Janette.M. Wing, Some notes on putting formal specifications to productive use, Science of Computer Programming, 2 (1) (1982), 53–68.

    Google Scholar 

  91. John V. Guttag and James J. Horning (editors), Larch: Languages and Tools for Formal Specification, Springer-Verlag, 1993.

    Google Scholar 

  92. John V Guttag, The Specification and Application to Programming of Abstract Data Types, PhD Thesis, Department of Computer Science, University of Toronto, 1975.

    Google Scholar 

  93. John V Guttag, Abstract data types and the development of data structures, Communications of the ACM, 20 (6) (1977), 396–404.

    Google Scholar 

  94. David Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, 8 (3) (1987), 231–274.

    MathSciNet  MATH  Google Scholar 

  95. Magne Haveraaen, Case study on algebraic software methodologies for scientific computing, Scientific Programming 8 (4) (2000), 261–273.

    Google Scholar 

  96. Matthew Hennessy, Algebraic Theory of Processes, MIT Press, 1988.

    Google Scholar 

  97. C A R Hoare and Cliff B. Jones, Essays in Computing Science, Prentice Hall International, 1989.

    Google Scholar 

  98. C A R Hoare, An axiomatic basis for computer programming, Communications of the ACM, 12 (10) (1969), 576–580, 583.

    Google Scholar 

  99. C A R Hoare, Communicating Sequential Processes, Communications of the ACM, 21 (8) (1978), 666–677.

    MATH  Google Scholar 

  100. C A R Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.

    Google Scholar 

  101. Gerard Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering 23 (5) (1997), 279–295.

    Google Scholar 

  102. Gerard Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2004.

    Google Scholar 

  103. Warren A Hunt, Jr, FM8501: A Verified Microprocessor, PhD Thesis, University of Texas at Austin, 1985.

    Google Scholar 

  104. C A R Hoare and N Wirth, An axiomatic definition of the programming language Pascal, Acta Informatica, 2 (4) (1973), 335–355.

    MATH  Google Scholar 

  105. Magne Haveraaen and Eric G. Wagner, Guarded algebras: disguising partiality so you won’t know whether it’s there, in (editors), in Didier Bert, Christine Choppy and Peter D. Mosses, Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science 1827, Springer-Verlag, 1999, 182–200.

    Google Scholar 

  106. Cliff Jones, Software Development: A Rigorous Approach, Prentice Hall International, 1980.

    Google Scholar 

  107. Cliff Jones, Development Methods for Computer Programs including a Notion of Interference. PhD Thesis, Oxford University, 1981. Published as: Programming Research Group, Technical Monograph 25.

    Google Scholar 

  108. Cliff Jones, Systematic Software Development using VDM, Prentice Hall 1990.

    Google Scholar 

  109. Cliff Jones, The Transition from VDL to VDM, Journal of Universal Computer Science, 7 (8) (2001), 631–640.

    MATH  Google Scholar 

  110. Cliff Jones, The early search for tractable ways of reasoning about programs, IEEE Annals of the History of Computing, 25 (2) (2003), 26–49.

    MathSciNet  Google Scholar 

  111. Capers Jones, The Technical and Social History of Software Engineering, Addison Wesley, 2013.

    Google Scholar 

  112. Joseph A Goguen and Rod Burstall, Introducing institutions, in Edward Clarke and Dexter Kozen (editors), Logics of Programming Workshop, Lecture Notes in Computer Science 164, Springer, 1984, 221–256.

    Google Scholar 

  113. Joseph A Goguen and Rod Burstall, Institutions: Abstract model theory for specification and programming, Journal of the Association for Computing Machinery, 39 (1) (1992), 95–146.

    Google Scholar 

  114. Alessandro Giacalone, Chi-chang Jou, and Scott A Smolka, Algebraic reasoning for probabilistic concurrent systems, in Manfred Broy and Cliff Jones (editors), Proceedings of IFIP Technical Committee 2 Working Conference on Programming Concepts and Methods, North Holland, 1990, 443–458.

    Google Scholar 

  115. Joseph A Goguen and Jose Meseguer, Security policies and security models, in Proceedings 1982 Symposium on Security and Privacy, Oakland, CA, IEEE Computer Society, 1982, 11–20.

    Google Scholar 

  116. Joseph A Goguen and Jose Meseguer, Inference control and unwinding, in Proceedings 1984 Symposium on Security and Privacy, Oakland, CA, IEEE Computer Society, 1984, 75–86.

    Google Scholar 

  117. Jan F Groote and M.R.Mousavi, Modeling and analysis of communicating systems, The MIT Press, 2014.

    Google Scholar 

  118. Joseph A Goguen, Memories of ADJ, Bulletin of the EATCS, No. 36, October 1989, 96–102. Also Current Trends in Theoretical Computer Science: Essays and Tutorials, World Scientific (1993), 76–81.

    Google Scholar 

  119. Michael Gordon, From LCF to HOL: a short history, in Gordon Plotkin, Colin P Stirling, and Mads Tofte (editors), Proof, Language, and Interaction, MIT Press, 2000, 169–185.

    Google Scholar 

  120. Michael Gordon, The unforeseen evolution of theorem proving in ARM processor verification. Talk at Swansea University, 28th April 2015. http://www.cl.cam.ac.uk/archive/mjcg/SwanseaTalk. Retrieved February 2018.

  121. Sheila A Greibach, Formal languages: origins and directions, IEEE Annals of the History of Computing, 3 (1) (1998), 14–41.

    Google Scholar 

  122. David Gries (editor), Programming Methodology. A Collection of Articles by Members of IFIP WG 2.3, Springer, 1978.

    Google Scholar 

  123. Joseph A Goguen, Jim W Thatcher, and Eric G Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R T Yeh (editor) Current Trends in Programming Methodology. IV: Data Structuring, Prentice-Hall, 1978, 80–149.

    Google Scholar 

  124. John Harrison, Josef Urban and Freek Wiedijk, History of interactive theorem proving, in Dov M. Gabbay, Jörg H Siekmann, and John Woods Handbook of the History of Logic. Volume 9: Computational Logic, North-Holland, 2014, 135–214.

    Google Scholar 

  125. Sam Kamin, Limits of the “algebraic” specification of abstract data types, ACM SIGPLAN Notices, 12 (10) (1977), 37–42.

    Google Scholar 

  126. B Kutzler and F Lichtenberger, Bibliography on Abstract Data Types, Lecture Notes in Computer Science 68, Springer, 1983.

    Google Scholar 

  127. Bakhadyr Khoussainov and Alexei Miasnikov, Finitely presented expansions of groups, semigroups, and algebras, Transactions American Mathematical Society, 366 (2014), 1455–1474.

    MathSciNet  MATH  Google Scholar 

  128. Deepak Kapur, David R Musser, and Alex A Stepanov, Tecton: A language for manipulating generic objects, in J. Staunstrup (editor), Program Specification, Lecture Notes in Computer Science 134, Springer-Verlag, 1982, 402–414.

    Google Scholar 

  129. Fred Kröger, LAR: A logic of algorithmic reasoning, Acta Informatica 8 (3) (1977), 243–266.

    MathSciNet  MATH  Google Scholar 

  130. Fred Kröger, Temporal Logic of Programs, EATCS Monographs in Theoretical Computer Science 8, Springer-Verlag, 1987.

    Google Scholar 

  131. Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems 16 (3) (1994), 872–923.

    Google Scholar 

  132. Carl Landwehr, Formal models for computer security, ACM Computing Surveys, 13 (3) (1981), 247–278.

    Google Scholar 

  133. Barbara Liskov, Russell Atkinson, Toby Bloom, J. Eliot Moss, J. Craig Schaffert, Robert Scheifler, and Alan Snyder, CLU Reference Manual, Computation Structures Group Memo 161, MIT Laboratory for Computer Science, Cambridge, MA, July 1978.

    Google Scholar 

  134. Peter Lauer, Consistent Formal Theories of the Semantics of Programming Languages, PhD Thesis, Queen’s University of Belfast, 1971. Published as TR 25.121, IBM Lab. Vienna.

    Google Scholar 

  135. Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf, Specification of Abstract Data Types: Mathematical Foundations and Practical Applications, John Wiley and Sons, 1996.

    Google Scholar 

  136. Barbara Liskov and John V Guttag, Abstraction and Specification in Program Development, MIT Press and McGraw Hill, 1986.

    Google Scholar 

  137. Gavin Lowe, Probabilistic and prioritized models of timed CSP. Theoretical Computer Science, 138 (1995), 315–352.

    MathSciNet  MATH  Google Scholar 

  138. Gavin Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software - Concepts and Tools, 17:93–102, 1996.

    Google Scholar 

  139. Barbara Liskov, Alan Snyder, Russell Atkinson, and J. Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, 20:8, 1977, 564–576.

    Google Scholar 

  140. Peter Lucas, On the semantics of programming languages and software devices, in Randall Rustin (editor), Formal Semantics of Programming Languages, Courant Computer Science Symposium 2, Prentice Hall, 1970, 52–57.

    Google Scholar 

  141. Peter Lucas, Formal Semantics of Programming Languages: VDL, IBM Journal of Research and Development 25 (5) (1981), 549–561.

    MATH  Google Scholar 

  142. Barbara Liskov and Stephen Zilles, Programming with abstract data types, ACM Sigplan Conference on Very High Level Languages, April 1974, 50–59.

    Google Scholar 

  143. Barbara Liskov and Stephen Zilles, Specification techniques for data abstractions, in IEEE Transactions on Software Engineering, 1 (1975), 7–19.

    Google Scholar 

  144. Carver A. Mead and Lynn Conway, Introduction to VLSI Systems, Addison-Wesley, 1980.

    Google Scholar 

  145. John McCarthy, Towards a mathematical science of computation, in Cicely M Popplewell (editor), Information Processing 1962, Proceedings of IFIP Congress 62, Munich, Germany, August 27 - September 1, 1962. North-Holland, 1962, 21–28.

    Google Scholar 

  146. John McCarthy, A basis for a mathematical theory of computation, in P Braffort and D Hirshberg (editors), Computer Programming and Formal Systems, North-Holland, 1963, 33–69.

    Google Scholar 

  147. John Mclean, Reasoning about security models, 1987 IEEE Symposium on Security and Privacy, Oakland, CA, IEEE Computer Society, 1987, 123–131.

    Google Scholar 

  148. Bertrand Meyer, Object-Oriented Software Construction, Prentice Hall, 1988.

    Google Scholar 

  149. Bertrand Meyer, Eiffel: The language, Prentice Hall, 1991.

    Google Scholar 

  150. Bertrand Meyer, Applying “Design by Contract”, IEEE Computer, 25 (10) 1992, 40–51.

    Google Scholar 

  151. Robin Milner, A Formal Notion of Simulation Between Programs, Memo 14, Computers and Logic Research Group, University College of Swansea, UK, 1970.

    Google Scholar 

  152. Robin Milner, Program Simulation: An Extended Formal Notion, Memo 15, Computers and Logic Research Group, University College of Swansea, UK, 1971.

    Google Scholar 

  153. Robin Milner, An Algebraic Definition of Simulation Between Programs, Stanford Computer Science Report No. STAN-CS-71-205, 1971.

    Google Scholar 

  154. Robin Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science 92, Springer-Verlag, 1980.

    Google Scholar 

  155. Robin Milner, Communication and Concurrency, Prentice Hall, 1989.

    Google Scholar 

  156. Robin Milner, Interview with Martin Berger at the University of Sussex, http://users.sussex.ac.uk/~mfb21/interviews/milner. Retrieved March 2019.

  157. F L Morris and Cliff B Jones, An early program proof by Alan Turing, Annals of the History of Computing, 6 (2) (1984), 139–143.

    Google Scholar 

  158. J Strother Moore, Tom Lynch and Matt Kaufmann, A mechanically checked proof of the correctness of the kernel of the AMD5\(_{K}\)86 floating-point division algorithm, IEEE Transactions on Computers 47 (9) (1998), 913–926.

    Google Scholar 

  159. R A Millo, R J Lipton, and A J Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, 22 (5) (1979), 271–280.

    Google Scholar 

  160. Carroll Morgan, Annabelle McIver, Karen Seidel and J. W. Sanders, Refinement-oriented probability for CSP, Formal Aspects of Computing, 8 (6) (1996) 617–647.

    Google Scholar 

  161. J Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, 5 (4) (1989), 461–492.

    Google Scholar 

  162. Peter D Mosses, The mathematical semantics of Algol 60, Oxford University Programming Research Group Technical Report 12, 1974.

    Google Scholar 

  163. Peter D. Mosses. The use of sorts in algebraic data type specification, in Michel Bidoit and Christine Choppy (editors), Recent Trends in Data Type Specification, Lecture Notes in Computer Science 655, Springer-Verlag, 1993, 66–91.

    Google Scholar 

  164. Peter D Mosses (editor), CASL Reference Manual. The Complete Documentation of the Common Algebraic Specification Language, Lecture Notes in Computer Science 2960, Springer-Verlag, 2004.

    Google Scholar 

  165. Till Mossakowski, The Distributed Ontology, Model and Specification Language DOL, in Phillip James and Markus Roggenbach (editors), Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science 10644, Springer-Verlag, 2017.

    Google Scholar 

  166. Thomas P Moran, The Command Language Grammar: A representation for the user interface of interactive computer systems, International Journal of Man-Machine Studies 15 (1) (1981), 3–50.

    Google Scholar 

  167. John McCarthy and J Painter, Correctness of a compiler for arithmetic expressions, Jacob T Schwartz (editor), Proceedings of Symposia in Applied Mathematics 19. Mathematical Aspects of Computer Science, American Mathematical Society, 1967, 33–41.

    Google Scholar 

  168. Robin Milner, Joachim Parrow and David Walker, A calculus of mobile processes, Information and Computation, 100 (1) (1992), 1–40.

    Google Scholar 

  169. Robert Milne and Christopher Strachey, A Theory of Programming Language Semantics. Part A: Indices and Appendices, Fundamental Concepts and Mathematical Foundations, Chapman and Hall, 1976.

    Google Scholar 

  170. Robert Milne and Christopher Strachey, A Theory of Programming Language Semantics. Part B: Standard Semantics, Store Semantics and Stack Semantics, Chapman and Hall, 1976.

    Google Scholar 

  171. Faron Moller and Georg Struth, Modelling Computing Systems: Mathematics for Computer Science, Springer, 2013.

    Google Scholar 

  172. Kevin McEvoy and John V Tucker, Theoretical foundations of hardware design, in Kevin McEvoy and John V Tucker (editors), Theoretical Foundations of VLSI Design, Cambridge Tracts in Theoretical Computer Science 10, Cambridge UP, 1990, 1–62.

    Google Scholar 

  173. Faron Moller and Chris Tofts, A temporal calculus of communicating systems, In Jos C. M. Baeten and Jan Willem Klop (editors), CONCUR 90, Theories of Concurrency: Unification and Extension, Lecture Notes in Computer Science 458. Springer-Verlag, 1990, 401–415.

    Google Scholar 

  174. Karl Meinke and John V Tucker, Universal algebra, in S. Abramsky, D. Gabbay and T Maibaum (editors) Handbook of Logic in Computer Science. Volume I: Mathematical Structures, Oxford University Press, 1992, 189–411.

    Google Scholar 

  175. Peter Naur et al. Report on the Algorithmic Language ALGOL60, Communications of the ACM, 3 (5) (1960), 299–314.

    Google Scholar 

  176. Peter Naur (editor), Revised Report on Algorithmic Language ALGOL 60, Communications of the ACM, i, No. I, (1962), 1–23.

    Google Scholar 

  177. Peter Naur, Proof of algorithms by general snapshots, BIT 6 (1966), 310–316.

    Google Scholar 

  178. Maurice Nivat, Infinite words, infinite trees, infinite computations, in J W de Bakker and J van Leeuwen (editors), Foundations of Computer Science III, Mathematical Centre Tracts 109, 1979, 3–52.

    Google Scholar 

  179. Peter Naur and Brian Randell (editors), Software Engineering: Report of a conference sponsored by the NATO Science Committee, Garmisch, Germany, 7-11 October, 1968, Brussels, Scientific Affairs Division, NATO (1969), 231pp.

    Google Scholar 

  180. Maurice Nivat and John Reynolds (editors), Algebraic Methods in Semantics, Cambridge University Press, 1985.

    Google Scholar 

  181. Roger Needham and Michael Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, 21(12) 1978, 993–999.

    Google Scholar 

  182. Susan Owicki and David Gries, An axiomatic proof technique for parallel programs I, Acta Informatica 6 (4) (1976), 319–340.

    Google Scholar 

  183. R Oliveira, P Palanque, B Weyers, J Bowen, A Dix, State of the art on formal methods for interactive systems, in B Weyers, J Bowen, A Dix, P Palanque (editors) The Handbook of Formal Methods in Human-Computer Interaction, Human–Computer Interaction Series. Springer, Cham, 2017.

    Google Scholar 

  184. Sam Owre, John Rushby and Natarajan Shankar, PVS: A Prototype Verification System, in Deepak Kapur (editor), 11th International Conference on Automated Deduction (CADE) Lecture Notes in Artificial Intelligence 607, Springer-Verlag, 1992, 748–752.

    Google Scholar 

  185. S. Owre, J.Rushby, N. Shankar, and F.von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS, IEEE Transactions on Software Engineering, 21(2) (1995), 107–125.

    Google Scholar 

  186. David Parnas, On the use of transition diagrams in the design of a user Interface for an interactive computer system, Proceedings 24th National ACM Conference (1969), 379–385.

    Google Scholar 

  187. David Parnas, A technique for software module specification with examples, Communications of the ACM, 15 (5) (1972), 330–336.

    Google Scholar 

  188. David Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, 15 (12)(1972), 1053–58.

    Google Scholar 

  189. David Park, Concurrency and automata on infinite sequences, in Peter Deussen (editor), Theoretical Computer science, Lecture Notes in Computer Science 104, Springer, 1981, 167–183.

    Google Scholar 

  190. David Parnas, Software Fundamentals – Collected Papers by David L Parnas, Daniel M.Hoffman and David M Weiss (editors), Addison-Wesley, 2001.

    Google Scholar 

  191. Gordon D. Plotkin, An operational semantics for CSP, in D Bjørner (editor), Proceedings IFIP TC2 Working Conference: Formal Description of Programming Concepts II, North-Holland, 1983, 199–223.

    Google Scholar 

  192. Gordon D. Plotkin, The origins of structural operational semantics, Journal of Logic and Algebraic Programming, 60-61, (2004), 3–15.

    Google Scholar 

  193. Gordon D. Plotkin, A structural approach to operational semantics, DAIMI FN-19, Computer Science Department, Aarhus University, 1981. Also: Journal of Logic and Algebraic Programming, 60-61, (2004), 17–139.

    Google Scholar 

  194. Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE 1977, 46–57.

    Google Scholar 

  195. Emil L. Post, Degrees of recursive unsolvability. Preliminary report, in Martin Davis (editor), Solvability, Provability, Definability: The Collected Works of Emil L. Post. Birkhäuser, Boston, Basel, Berlin, 1994, 549–550.

    Google Scholar 

  196. J.-P. Queille and Josef Sifakis, Specification and verification of concurrent systems in CESAR. In: Symposium on Programming. Lecture Notes in Computer Science, vol. 137, Springer, 1982, 337–351.

    Google Scholar 

  197. Brian Randell and John N. Buxton (editors), Software Engineering Techniques: Report of a conference sponsored by the NATO Science Committee, Rome, Italy, 27-31 October, 1969, Brussels, Scientific Affairs Division, NATO (1970), 164pp.

    Google Scholar 

  198. Willem-Paul de Roever, Frank de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers, Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge University Press, 2001.

    Google Scholar 

  199. Phyllis Reisner, Formal grammar and human factors design of an interactive graphics system, IEEE Transactions on Software Engineering, 7 (2) (1981), 229–240.

    Google Scholar 

  200. Horst Reichel, Initial Computability Algebraic Specifications, and Partial Algebras, Clarendon Press, 1987.

    Google Scholar 

  201. Markus Roggenbach, Mila Majster-Cederbaum, Towards a unified view of bisimulation: a comparative study. Theoretical Computer Science, 238 (2000), 81–130.

    Google Scholar 

  202. A W Roscoe, Model checking CSP, in A Classical Mind: Essays in Honour of C A R Hoare, Prentice Hall, 1994, 353–2378.

    Google Scholar 

  203. A W Roscoe, Theory And Practice Of Concurrency, Prentice Hall, 1997.

    Google Scholar 

  204. A W Roscoe, Understanding Concurrent Systems, Springer, 2010.

    Google Scholar 

  205. Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Cambridge UP, 2011.

    Google Scholar 

  206. Ben Shneiderman, Multi-party grammars and related features for defining interactive systems. IEEE Transactions on Systems, Man, and Cybernetics, 12 (2) (1982), 148–154.

    Google Scholar 

  207. Davide Sangiorgi and Jan Rutten (editors), Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science 52, Cambridge UP, 2011.

    Google Scholar 

  208. Viggo Stoltenberg-Hansen and John V Tucker, Effective algebras, in S Abramsky, D Gabbay and T Maibaum (editors) Handbook of Logic in Computer Science. Volume IV: Semantic Modelling, Oxford University Press, 1995, 357–526.

    Google Scholar 

  209. Donald Sannella and Andrzej Tarlecki, Foundations of Algebraic Specification and Formal Software Development, EATCS Monographs in Theoretical Computer Science, Springer, 2012.

    Google Scholar 

  210. T B Steel (editor), Formal Language Description Languages for Computer Programming, North-Holland, 1966.

    Google Scholar 

  211. Bjarne Stroustrup, Classes: An abstract data type facility for the C language. Bell Laboratories Computer Science Technical Report, CSTR 84. April 1980.

    Google Scholar 

  212. Bernard Sufrin, Formal specification of a display editor, Science of Computer Programming, 1(1982), 157–202.

    Google Scholar 

  213. Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press, 2003.

    Google Scholar 

  214. Margaret Tierney, Software engineering standards: the ‘formal methods debate’ in the UK, Technology Analysis and Strategic Management 4 (3), (1992), 245–278

    Google Scholar 

  215. Harold W Thimbleby and Michael Harrison, Formal Methods in Human-Computer Interaction, Cambridge UP, 1990.

    Google Scholar 

  216. Harold W Thimbleby, User interface design and formal methods, Computer Bulletin, series III, 2 (3) (1986) 13–15, 18.

    Google Scholar 

  217. Harold W Thimbleby, User Interface Design, ACM Press, Addison-Wesley, 1990.

    Google Scholar 

  218. Harold W Thimbleby, Death by Design: Stories of digital healthcare, in preparation.

    Google Scholar 

  219. John V Tucker and Jeffrey I Zucker, Program Correctness over Abstract Data Types with Error-state Semantics, North-Holland, Amsterdam, 1988.

    Google Scholar 

  220. John V Tucker and Jeffrey I Zucker, Computable functions and semicomputable sets on many sorted algebras, in S. Abramsky, D. Gabbay and T Maibaum (editors), Handbook of Logic for Computer Science. Volume V: Logical and Algebraic Methods, Oxford University Press, 2000, 317–523.

    Google Scholar 

  221. John V Tucker and Jeffrey I Zucker, Origins of our theory of computation on abstract data types at the Mathematical Centre, Amsterdam, 1979-80, in F de Boor, M van der Heijden, P Klint, J Rutten (eds), Liber Amicorum: Jaco de Bakker, CWI Amsterdam, 2002, 197–221.

    Google Scholar 

  222. Jeffrey Ullman and John E. Hopcroft, Formal Languages and Their Relation to Automata, Addison Wesley, 1969.

    Google Scholar 

  223. Eric G. Wagner, Algebraic specifications: some old history, and new thoughts, Unpublished, 2001.

    Google Scholar 

  224. B Weyers, J Bowen, A Dix, P Palanque (editors) The Handbook of Formal Methods in Human-Computer Interaction, Human Computer Interaction Series, Springer, Cham, 2017.

    Google Scholar 

  225. Edward Yourdon, Writings of the Revolution: Selected Readings on Software Engineering, Yourdon Press, 1982.

    Google Scholar 

  226. Steve Zilles, Algebraic specifications of data types, Project MAC Progress Report 11, Massachusetts Institute of Technology, Cambridge, MA, 1974, 52–58.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swansea University, Wales, UK

    John V. Tucker

Authors
  1. John V. Tucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Tucker, J.V. (2022). Origins and Development of Formal Methods. In: Formal Methods for Software Engineering. Texts in Theoretical Computer Science. An EATCS Series. Springer, Cham. https://doi.org/10.1007/978-3-030-38800-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-38800-3_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-38799-0

  • Online ISBN: 978-3-030-38800-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation