F.S. de Boer
- Verification of sequential and concurrent programs: 3rd ed.
- Number of pages
- London: Springer
- Texts in computer science
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
Computer programs are an indispensable part of many of the systems we rely upon in our daily lives, and the proper functioning and safety of these systems is of paramount importance. The development of methods that ensure program correctness is therefore a key challenge for computer scientists.
This third edition of Verification of Sequential and Concurrent Programs provides a systematic exploration of one of the most common approaches to program verification, known as the "assertional" approach. Following the successful formula of previous editions, this approach is applied to deterministic and nondeterministic sequential programs of varying complexity, together with both parallel and distributed concurrent programs. The expanded content of this thorough new edition also includes coverage of the verification of object-oriented programs. For each class of programs, the authors introduce an operational semantics and proof systems for the verification of partial and total correctness, justified formally in corresponding soundness theorems. Case studies supplied throughout the book demonstrate the use of the proof systems to formally verify solutions to classical problems, such as sorting, manipulation of lists, producer/consumer and mutual exclusion.
- go to publisher's site
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.