Verification of Sequential and Concurrent Programs

Front Cover
Springer-Verlag, 1991 - Computers - 441 pages
This book provides a structural introduction to program verification. Sequential programs in the form of deterministic and nondeterministic programs, and concurrent programs in the form of parallel and distributed programs, are considered within the context of their partial and total correctness. While other books have covered verification and semantics of sequential programs, this is the first book to address verification and semantics of structured concurrent programs. The book is appropriate for either a one- or two-semester introductory course on program verification for upper division of undergraduate studies or graduate students. It can also be used as an introduction to operational semantics. Outlines of possible one-semester courses are presented in the preface of the book. Within these chapters, the authors systematically discuss five classes of programs, concentrating on operational semantics, syntax directed assertional proof systems, soundness proofs of the proof systems, program transformations, correctness proofs of the program transformations, and correctness proofs of a substantial example. Each chapter is developed in a systematic and easy-to-understand manner and closes with a list of exercises. The material presented here draws on work which until now was only available in the form of advanced research publications. A large portion of the material is entirely new. This book provides an introduction to the subject which also will lead to current research problems in the areas considered.

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.


Deterministic Programs

8 other sections not shown

Other editions - View all

Common terms and phrases

About the author (1991)

Krzysztof R. Apt received his PhD in 1974 in mathematical logic from the University of Warsaw in Poland. He is a senior researcher at CWI, Amsterdam and Professor of Computer Science at the University of Amsterdam. He is the author of three other books: Verification of Sequential and Concurrent Programs (with E.-R. Olderog), From Logic Programming to Prolog, and Principles of Constraint Programming, and has published 50 journal articles and 15 book chapters. He is the founder and the first editor-in-chief of the ACM Transactions on Computational Logic, and past president of the Association for Logic Programming. He is a member of the Academia Europaea (Mathematics and Informatics Section).

E.-R. Olderog is Professor of Computer Science at the University of Oldenburg, Germany. In 1994 he was awarded the Leibniz Prize of the German Research Council (DFG).

Bibliographic information