Verification by Abstract Interpretation, Soundness and Abstract Induction

Automatic program verification tools have to cope with program-ming language and machine semantics, undecidability, and mathe-matical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation [18, 19, 22]. Programming language semantics If Edsger W. Dijkstra could claim in his 1972 Turing lecture [29, p. 863] that “When FORTRAN has been called an infantile disorder, full PL/1, with its growth characteristics of a dangerous tumor, could turn out to be a fatal disease.”, PL/1 and its 1000 pages formal operational semantics defined in VDL [7] now appears as a marvel of simplicity compared to present-day programming languages [57] and their informal definitions [1]. The formal specification of the semantics of programming lan