Skip to main content
Book cover

Verification of Sequential and Concurrent Programs

  • Textbook
  • © 2009

Overview

  • Deals with the verification of programs allowing dynamic process creation
  • Includes four new chapters on increasingly important aspects of programming
  • Contains many learning tools to aid the reader such as case studies, exercises, comprehensive references/further reading and helpful appendices

Part of the book series: Texts in Computer Science (TCS)

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

Access this book

eBook USD 69.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 109.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

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (12 chapters)

  1. In the Beginning

  2. Deterministic Programs

  3. Parallel Programs

  4. Nondeterministic and Distributed Programs

Keywords

About this book

HIS BOOK CONTAINS a most comprehensive text that presents syntax-directed and compositional methods for the formal veri?- T cation of programs. The approach is not language-bounded in the sense that it covers a large variety of programming models and features that appear in most modern programming languages. It covers the classes of - quential and parallel, deterministic and non-deterministic, distributed and object-oriented programs. For each of the classes it presents the various c- teria of correctness that are relevant for these classes, such as interference freedom, deadlock freedom, and appropriate notions of liveness for parallel programs. Also, special proof rules appropriate for each class of programs are presented. In spite of this diversity due to the rich program classes cons- ered, there exist a uniform underlying theory of veri?cation which is synt- oriented and promotes compositional approaches to veri?cation, leading to scalability of the methods. The text strikes the proper balance between mathematical rigor and - dactic introduction of increasingly complex rules in an incremental manner, adequately supported by state-of-the-art examples. As a result it can serve as a textbook for a variety of courses on di?erent levels and varying durations. It can also serve as a reference book for researchers in the theory of veri?- tion, in particular since it contains much material that never before appeared in book form. This is specially true for the treatment of object-oriented p- grams which is entirely novel and is strikingly elegant.

Reviews

"The Third Edition is an excellent new version of a valuable book. Enhanced with new material on recursion and object-oriented programs, this book now covers methods for verifying sequential, object-oriented, and concurrent programs using well-chosen sample programming languages that highlight fundamental issues and avoid incidental complications. With growing challenges today to produce correct software systems for the future, this book lets students wisely use a few months now to master concepts that will last them a lifetime." (John C. Mitchell, Stanford University)

"Verification of programs is the Holy Grail of Computer Science. This book makes its pursuit seem both pleasant and worthwhile. Its unique strength lies in the way the authors have deconstructed the apparently complex subject such that each piece carries exactly one idea. The beauty of the presentation extends from the overall structure of the book to the individual explanations, definitions and proofs." (Andreas Podelski, University of Freiburg)

"Program verification became an interesting research topic of computing science about forty years ago. Research literature on this topic has grown quickly in accordance with rapid development of various programming paradigms. Therefore it has been a challenge to university lecturers on program verification how to carefully select an easy but comprehensive approach, which can fit in with most programming paradigms and can be taught in a systematic way. The publication of this book is an answer to the challenge, and to my knowledge quite many university lecturers have been influenced by the earlier editions of this book if not chosen them as textbook. Given that the third edition includes verification of object-oriented programs – the most fashionable programming paradigm, and presents it in a way coherent with the approach adopted by the earlier ones, we can expect a further impact of the new edition on university teachings." (ZhouChaochen, Chinese Academy of Sciences, Beijing)

Authors and Affiliations

  • Centrum Wiskunde & Informatica, Amsterdam, Netherlands

    Krzysztof R. Apt, Frank S. Boer

  • Department für Informatik, Universität Oldenburg, Oldenburg, Germany

    Ernst-Rüdiger Olderog

Bibliographic Information

  • Book Title: Verification of Sequential and Concurrent Programs

  • Authors: Krzysztof R. Apt, Frank S. Boer, Ernst-Rüdiger Olderog

  • Series Title: Texts in Computer Science

  • DOI: https://doi.org/10.1007/978-1-84882-745-5

  • Publisher: Springer London

  • eBook Packages: Computer Science, Computer Science (R0)

  • Copyright Information: Springer-Verlag London Limited 2009

  • Hardcover ISBN: 978-1-84882-744-8Published: 05 October 2009

  • Softcover ISBN: 978-1-4471-2513-6Published: 14 March 2012

  • eBook ISBN: 978-1-84882-745-5Published: 18 September 2009

  • Series ISSN: 1868-0941

  • Series E-ISSN: 1868-095X

  • Edition Number: 3

  • Number of Pages: XXIV, 502

  • Number of Illustrations: 26 b/w illustrations

  • Additional Information: Originally published in the series: Graduate Texts in Computer Science

  • Topics: Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Algorithm Analysis and Problem Complexity

Publish with us