Verification of sequential and concurrent programs / Krzysztof R. Apt / Ernst-Rüdiger Olderog [ Livre]

Auteur principal: Apt, Krzysztof R.Co-auteur: Olderog, Ernst-RüdigerLangue: Anglais ; de l'oeuvre originale, Anglais.Mention d'édition: 2nd ed.Publication : New York : Springer, 1997Description : XVII-364 pages ; 25 cmISBN: 0387948961.Collection: Graduate texts in computer scienceClassification: 004.14 Théorie des langages de programmationRésumé: Computer programs are becoming more and more part of systems that we rely on in our daily lives. The proper functioning and safety of these systems is of paramount importance. A major challenge for computer science is to develop methods that ensure program correctness. This textbook addresses this problem by providing a structured introduction to program verification. It uses one of the most common approaches, called the assertional method, because it relies on the use of assertions that are attached to program control points. Sequential programs in the form of deterministic and nondeterministic programs, and concurrent programs in the form of parallel and distributed programs are considered together with proof systems for the verification of their partial and total correctness. The use of these proof systems is demonstrated with the help of case studies. In particular, solutions to classical problems such as producer/consumer and mutual exclusion are formally verified. Each chapter is developed in a systematic and easy-to-understand manner and concludes with exercises and bibliographic remarks for further reading. As a result, this textbook will be appropriate for either an introductory course on program verification for the upper division of undergraduate studies or for graduate studies. It can also be used as an introduction to operational semantics of programming languages..Sujet - Nom commun: Logiciels -- Vérification | Traitement réparti | Programmation parallèle (informatique) | Logiciels -- Développement
Current location Call number Status Notes Date due Barcode
ENS Rennes - Bibliothèque
Informatique
004.14 APT (Browse shelf) Available 004.14 Théorie des langages de programmation 00003129
ENS Rennes - Bibliothèque
Informatique
004.14 APT (Browse shelf) Exclu du prêt 004.14 Théorie des langages de programmation 000031291
ENS Rennes - Bibliothèque
Informatique
004.14 APT (Browse shelf) Available 004.14 Théorie des langages de programmation 000031292

Bibliogr. p. [343]-352. Index

Computer programs are becoming more and more part of systems that we rely on in our daily lives. The proper functioning and safety of these systems is of paramount importance. A major challenge for computer science is to develop methods that ensure program correctness. This textbook addresses this problem by providing a structured introduction to program verification. It uses one of the most common approaches, called the assertional method, because it relies on the use of assertions that are attached to program control points. Sequential programs in the form of deterministic and nondeterministic programs, and concurrent programs in the form of parallel and distributed programs are considered together with proof systems for the verification of their partial and total correctness. The use of these proof systems is demonstrated with the help of case studies. In particular, solutions to classical problems such as producer/consumer and mutual exclusion are formally verified. Each chapter is developed in a systematic and easy-to-understand manner and concludes with exercises and bibliographic remarks for further reading. As a result, this textbook will be appropriate for either an introductory course on program verification for the upper division of undergraduate studies or for graduate studies. It can also be used as an introduction to operational semantics of programming languages.

Powered by Koha