Ji:I was doing my homework, and then I found a wikipedia entry about List of important publications in Computer Science. I think it is always good to see that how a successful topic was created and breakthrough was made. Apparently, not so many people can achieve even one, but it would be a pity that few people think about to do at least one.
- Topic creator – A publication that created a new topic
- Breakthrough – It changed scientific knowledge significantly
- Introduction – It is a good introduction or survey of a topic
- Influence – It has significantly influenced the world
- Latest and greatest – The current most advanced result in a topic
Formal verification
[edit] On computable numbers, with an application to the Entscheidungsproblem
- Alan Turing
- Proceedings of the London Mathematical Society, Series 2, 42 (submitted May 28, 1936, read November 12, 1936), pp 230–265. Errata appeared in Series 2, 43 (1937), pp 544–546.
- Online version (MS IExplorer only)
- PDF version of above page (verified to display properly with xpdf and acroread)
Description: In his paper on the Entscheidungsproblem, Alan Turing introduces the idea of a Turing Machine which he uses to prove the undecidability of the Halting Problem and (consequently) the undecidability of first-order logic (because if FOL were decidable then the Halting Problem would be decidable). This is the first of a series of so-called “negative” results formally proving that the set of all possible programs does not include a program V that is able to decide the formal correctness of (i.e. formally verify) any given program P – any attempt to write a “program verifier” V (always returning a yes/no result in a finite time) is therefore futile because the problem is provably impossible. However, it is still possible to write a program V’ (returning a yes/no/maybe result) that is able to formally verify some programs but not all programs, even if it is not possible to define in advance exactly for which programs V’ will be able to return “yes/no” rather than “maybe”.
Importance: Breakthrough
[edit] Assigning Meaning to Programs
- Robert Floyd
- Mathematical Aspects of Computer Science, pages 19–32, 1967
- scanned copy (bad quality, taken from External Link section at Robert Floyd)
Description: Robert Floyd’s landmark paper Assigning Meaning to Programs introduces the method of inductive assertions and describes how a program annotated with first-order assertions may be shown to satisfy a pre- and post-condition specification – the paper also introduces the concepts of loop invariant and verification condition.
Importance: Topic creator
[edit] An Axiomatic Basis for Computer Programming
- C.A.R. Hoare
- Communications of the ACM, 12:576–580, 1969
- online version (PDF)
Description: Tony Hoare’s paper An Axiomatic Basis for Computer Programming describes a set of inference (i.e. formal proof) rules for fragments of an Algol-like programming language described in terms of (what are now called) Hoare-triples.
Importance: Breakthrough
[edit] Guarded Commands, Nondeterminacy and Formal Derivation of Programs
- Edsger W. Dijkstra
- 1975
Description: Edsger Dijkstra’s paper Guarded Commands, Nondeterminacy and Formal Derivation of Programs (expanded by his 1976 postgraduate-level textbook A Discipline of Programming) proposes that, instead of formally verifying a program after it has been written (i.e. post facto), programs and their formal proofs should be developed hand-in-hand (using predicate transformers to progressively refine weakest pre-conditions), a method known as program (or formal) refinement (or derivation), or sometimes “correctness-by-construction”.
Importance: Topic creator
[edit] Proving Assertions about Parallel Programs
- Edward A. Ashcroft
- J. Comput. Syst. Sci. 10(1): 110-135 (1975)
Description: The paper that introduced invariance proofs of concurrent programs.
Importance: Breakthrough
[edit] An Axiomatic Proof Technique for Parallel Programs I
- Susan S. Owicki, David Gries
- Acta Inf. 6: 319-340 (1976)
Description: In this paper, along with the same authors paper “Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285 (1976)”, the axiomatic approach to parallel programs verification was presented.
Importance: Breakthrough
[edit] A Discipline of Programming
- Edsger W. Dijkstra
- 1976
Description: Edsger Dijkstra’s classic postgraduate-level textbook A Discipline of Programming extends his earlier paper Guarded Commands, Nondeterminacy and Formal Derivation of Programs and firmly establishes the principle of formally deriving programs (and their proofs) from their specification.
Importance: Influence
[edit] Denotational Semantics
- Joe Stoy
- 1977
Description: Joe Stoy’s Denotational Semantics is the first (postgraduate level) book-length exposition of the mathematical (or functional) approach to the formal semantics of programming languages (in contrast to the operational and algebraic approaches).
Importance: Introduction
[edit] The Temporal Logic of Programs
- Amir Pnueli
- In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.
Description: The use of temporal logic was suggested as a method for formal verification.
Importance: Topic creator, Impact
[edit] Time, clocks, and the ordering of events in a distributed system
- Leslie Lamport
- CACM, 21(7):558– 565, July 1978
- online version(PDF)
Description: The ordering of events is critical to consistency and correctness of many algorithms used in distributed computer systems. This paper discusses how such ordering can be managed consistently and introduces a set of rules for managing virtual time in such systems. These rules are the basis for many subsequent algorithms for ordering events in distributed system.
Importance: Influence
[edit] Communicating Sequential Processes (1978)
- C.A.R. Hoare
- 1978
Description: Tony Hoare’s (original) Communicating Sequential Processes (CSP) paper introduces the idea of concurrent processes (i.e. programs) that do not share variables but instead cooperate solely by exchanging synchronous messages.
Importance: Influence
[edit] A Calculus of Communicating Systems
- Robin Milner
- 1980
Description: Robin Milner’s A Calculus of Communicating Systems (CCS) paper describes a process algebra permitting systems of concurrent processes to be reasoned about formally, something which has not been possible for earlier models of concurrency (semaphores, critical sections, original CSP).
Importance: Breakthrough
[edit] Software Development: A Rigorous Approach
- Cliff Jones
- 1980
Description: Cliff Jones’ textbook Software Development: A Rigorous Approach is the first full-length exposition of the Vienna Development Method (VDM), which has evolved (principally) at IBM’s Vienna research lab over the previous decade and which combines the idea of program refinement as per Dijkstra with that of data refinement (or reification) whereby algebraically-defined abstract data types are formally transformed into progressively more “concrete” representations.
Importance: Influence
[edit] The Science of Programming
- David Gries
- 1981
Description: David Gries’ textbook The Science of Programming describes Dijkstra’s weakest precondition method of formal program derivation, except in a very much more accessible manner than Dijkstra’s earlier A Discipline of Programming.
Importance: Introduction
[edit] Communicating Sequential Processes (1985)
- C.A.R. Hoare
- 1985
Description: Tony Hoare’s Communicating Sequential Processes (CSP) textbook (currently the third most cited computer science reference of all time) presents an updated CSP model in which cooperating processes do not even have program variables and which, like CCS, permits systems of processes to be reasoned about formally.
Importance: Influence
[edit] A Calculus of Mobile Processes (1989)
Description: This paper introduces the Pi-Calculus, a generalisation of CCS which allows process mobility. The calculus is extremely simple and has become the dominant paradigm in the theoretical study of programming languages, typing systems and program logics.
Importance: Breakthrough
[edit] The Z Notation: A Reference Manual
Description: Mike Spivey’s classic textbook The Z Notation: A Reference Manual summarises the formal specification language Z which, although originated by Jean-Raymond Abrial, has evolved (principally) at Oxford University over the previous decade (Z may ultimately become by far the most widely used language of its kind).
Importance: Influence
[edit] Communication and Concurrency
- Robin Milner
- Prentice-Hall International, 1989
Description: Robin Milner’s textbook Communication and Concurrency is a more accessible, although still technically advanced, exposition of his earlier CCS work.
Importance: Introduction
Related posts:
- Paper accepted finally My joint paper with Wiebe and Mike with title “Verification...
Related posts brought to you by Yet Another Related Posts Plugin.
Impressive: The list of topics leading to the present practices of formal verification, model-checking and theorem-proving.
Suppose there was a new system of logic–reactive to external events–that is not a Turing machine, but nevertheless can manage and use Turing machines. The new system is inherently parallel-concurrent.
Hi, thank you for your comment. This list is borrowed from Wikipedia.
I thought we can have concurrent turing machines long time ago. It will be great if we could invente a competely different computation model.