Formal specification and verification

Stephan Merz

Abstract

Beyond his seminal contributions to the theory and the design of concurrent and distributed algorithms, Leslie Lamport has throughout his career worked on methods and formalisms for rigorously establishing the correctness of algorithms. Commenting on his first article about a method for proving the correctness of multi-process programs on the website providing access to his collected writings, Lamport recalls that this interest originated in his submitting a flawed mutual-exclusion algorithm in the early 1970s. As a trained mathematician, Lamport is perfectly familiar with mathematical set theory, the standard formal foundation of classical mathematics. His career in industrial research environments and the fact that his main interest has been in algorithms, not formalisms, has certainly contributed to his designing reasoning methods that combine pragmatism and mathematical elegance. The methods that he designed have always been grounded in the semantics of programs and their executions rather than being driven by the syntax in which these programs are expressed, in contrast to many methods advocated by ``pure'' computer scientists.

Available as: PDF

Reference

@incollection{merz:lamport-book,
  author    = {Stephan Merz},
  editor    = {Dahlia Malkhi},
  title     = {Formal specification and verification},
  booktitle = {Concurrency: the Works of Leslie Lamport},
  pages     = {103--129},
  publisher = {ACM},
  year      = {2019},
}