Verification of Sequential and Concurrent Programs

By: Krzysztof R. Apt, Amir Pnueli (Foreword by), Frank S. de Boer

Write A Review

Hardcover | 5 October 2009 | Edition Number 3

At a Glance

Hardcover
528 Pages

Edition Type
Revised

Dimensions(cm)
24.13 x 16.51 x 3.18

Hardcover

$169.00

or 4 interest-free payments of $42.25 with

Ships in 5 to 7 business days

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.

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Computing & I.T.Computer Programming & Software Development Software Engineering Software Testing & Verification Algorithms & Data Structures Computer Science Computer Architecture & Logic Design Mathematics Mathematical Foundation Mathematical Logic

Other Editions and Formats

Paperback

Published: 14th March 2012

View Product

Endorsements	p. v
Foreword	p. vii
Preface	p. ix
Outlines of One-semester Courses	p. xiv
In the Beginning
Introduction	p. 3
An Example of a Concurrent Program	p. 4
Solution 1	p. 4
Solution 2	p. 5
Solution 3	p. 6
Solution 4	p. 8
Solution 5	p. 9
Solution 6	p. 10
Program Correctness	p. 11
Structure of this Book	p. 13
Automating Program Verification	p. 16
Assertional Methods in Practice	p. 17
Preliminaries	p. 19
Mathematical Notation	p. 21
Sets	p. 21
Tuples	p. 22
Relations	p. 23
Functions	p. 23
Sequences	p. 24
Strings	p. 25
Proofs	p. 26
Induction	p. 27
Grammars	p. 29
Typed Expressions	p. 29
Types	p. 29
Variables	p. 30
Constants	p. 30
Expressions	p. 31
Subscripted Variables	p. 32
Semantics of Expressions	p. 32
Fixed Structure	p. 33
States	p. 34
Definition of the Semantics	p. 35
Updates of States	p. 36
Formal Proof Systems	p. 38
Assertions	p. 39
Semantics of Assertions	p. 41
Substitution	p. 42
Substitution Lemma	p. 47
Exercises	p. 50
Bibliographic Remarks	p. 51
Deterministic Programs
while Programs	p. 55
Syntax	p. 57
Semantics	p. 58
Properties of Semantics	p. 62
Verification	p. 63
Partial Correctness	p. 65
Total Correctness	p. 70
Decomposition	p. 73
Soundness	p. 73
Proof Outlines	p. 79
Partial Correctness	p. 79
Total Correctness	p. 83
Completeness	p. 85
Parallel Assignment	p. 91
Failure Statement	p. 94
Auxiliary Axioms and Rules	p. 97
Case Study: Partitioning an Array	p. 99
Systematic Development of Correct Programs	p. 113
Summation Problem	p. 115
Case Study: Minimum-Sum Section Problem	p. 116
Exercises	p. 121
Bibliographic Remarks	p. 124
Recursive Programs	p. 127
Syntax	p. 129
Semantics	p. 129
Properties of the Semantics	p. 131
Verification	p. 132
Partial Correctness	p. 132
Total Correctness	p. 134
Decomposition	p. 137
Discussion	p. 138
Soundness	p. 139
Case Study: Binary Search	p. 144
Partial Correctness	p. 145
Total Correctness	p. 147
Exercises	p. 149
Bibliographic Remarks	p. 150
Recursive Programs with Parameters	p. 151
Syntax	p. 152
Semantics	p. 154
Verification	p. 157
Partial Correctness: Non-recursive Procedures	p. 158
Partial Correctness: Recursive Procedures	p. 162
Modularity	p. 165
Total Correctness	p. 165
Soundness	p. 167
Case Study: Quicksort	p. 172
Formal Problem Specification	p. 173
Properties of Partition	p. 173
Auxiliary Proof: Permutation Property	p. 174
Auxiliary Proof: Sorting Property	p. 175
Total Correctness	p. 180
Exercises	p. 182
Bibliographic Remarks	p. 182
Object-Oriented Programs	p. 185
Syntax	p. 187
Local Expressions	p. 187
Statements and Programs	p. 188
Semantics	p. 192
Semantics of Local Expressions	p. 192
Updates of States	p. 194
Semantics of Statements and Programs	p. 195
Assertions	p. 197
Substitution	p. 199
Verification	p. 200
Partial Correctness	p. 201
Total Correctness	p. 204
Adding Parameters	p. 206
Semantics	p. 207
Partial Correctness	p. 208
Total Correctness	p. 210
Transformation of Object-Oriented Programs	p. 211
Soundness	p. 214
Object Creation	p. 217
Semantics	p. 218
Assertions	p. 219
Verification	p. 223
Soundness	p. 225
Case Study: Zero Search in Linked List	p. 226
Partial Correctness	p. 226
Total Correctness	p. 229
Case Study: Insertion into a Linked List	p. 232
Exercises	p. 238
Bibliographic Remarks	p. 240
Parallel Programs
Disjoint Parallel Programs	p. 245
Syntax	p. 247
Semantics	p. 248
Determinism	p. 249
Sequentialization	p. 252
Verification	p. 253
Parallel Composition	p. 254
Auxiliary Variables	p. 256
Soundness	p. 259
Case Study: Find Positive Element	p. 261
Exercises	p. 264
Bibliographic Remarks	p. 266
Parallel Programs with Shared Variables	p. 267
Access to Shared Variables	p. 269
Syntax	p. 270
Semantics	p. 271
Atomicity	p. 272
Verification: Partial Correctness	p. 274
Component Programs	p. 274
No Compositionality of Input/Output Behavior	p. 275
Parallel Composition: Interference Freedom	p. 276
Auxiliary Variables Needed	p. 279
Soundness	p. 282
Verification: Total Correctness	p. 284
Component Programs	p. 284
Parallel Composition: Interference Freedom	p. 286
Soundness	p. 288
Discussion	p. 289
Case Study: Find Positive Element More Quickly	p. 291
Allowing More Points of Interference	p. 294
Case Study: Parallel Zero Search	p. 299
Simplifying the program	p. 299
Proving partial correctness	p. 300
Exercises	p. 303
Bibliographic Remarks	p. 305
Parallel Programs with Synchronization	p. 307
Syntax	p. 309
Semantics	p. 310
Verification	p. 311
Partial Correctness	p. 311
Weak Total Correctness	p. 313
Total Correctness	p. 314
Soundness	p. 316
Case Study: Producer/Consumer Problem	p. 319
Case Study: The Mutual Exclusion Problem	p. 324
Problem Formulation	p. 324
Verification	p. 326
A Busy Wait Solution	p. 327
A Solution Using Semaphores	p. 331
Allowing More Points of Interference	p. 334
Case Study: Synchronized Zero Search	p. 335
Simplifying the Program	p. 336
Decomposing Total Correctness	p. 337
Proving Termination	p. 337
Proving Partial Correctness	p. 342
Exercises	p. 344
Bibliographic Remarks	p. 345
Nondeterministic and Distributed Programs
Nondeterministic Programs	p. 349
Syntax	p. 351
Semantics	p. 352
Properties of Semantics	p. 353
Why Are Nondeterministic Programs Useful?	p. 354
Symmetry	p. 355
Nondeterminism	p. 355
Failures	p. 356
Modeling Concurrency	p. 356
Verification	p. 357
Partial Correctness	p. 357
Total Correctness	p. 357
Soundness	p. 359
Case Study: The Welfare Crook Problem	p. 360
Transformation of Parallel Programs	p. 363
Exercises	p. 368
Bibliographic Remarks	p. 370
Distributed Programs	p. 373
Syntax	p. 375
Sequential Processes	p. 375
Distributed Programs	p. 376
Semantics	p. 380
Transformation into Nondeterministic Programs	p. 382
Semantic Relationship Between S and T(S)	p. 382
Proof of the Sequentialization Theorem	p. 385
Verification	p. 390
Partial Correctness	p. 390
Weak Total Correctness	p. 391
Total Correctness	p. 391
Proof Systems	p. 392
Soundness	p. 393
Case Study: A Transmission Problem	p. 396
Decomposing Total Correctness	p. 397
Proving Partial Correctness	p. 397
Proving Absence of Failures and of Divergence	p. 399
Proving Deadlock Freedom	p. 400
Exercises	p. 402
Bibliographic Remarks	p. 405
Fairness	p. 407
The Concept of Fairness	p. 409
Selections and Runs	p. 410
Fair Nondeterminism Semantics	p. 412
Transformational Semantics	p. 413
Well-Founded Structures	p. 413
Random Assignment	p. 414
Semantics	p. 415
Verification	p. 415
Schedulers	p. 419
The Scheduler FAIR	p. 421
The Scheduler RORO	p. 424
The Scheduler QUEUE	p. 426
Transformation	p. 427
Verification	p. 430
Total Correctness	p. 430
Soundness	p. 438
Case Study: Zero Search	p. 442
Case Study: Asynchronous Fixed Point Computation	p. 446
Exercises	p. 452
Bibliographic Remarks	p. 455
Semantics	p. 457
Axioms and Proof Rules	p. 459
Proof Systems	p. 471
Proof Outlines	p. 475
References	p. 477
Index	p. 491
Author Index	p. 497
Symbol Index	p. 501
Table of Contents provided by Ingram. All Rights Reserved.

Verification of Sequential and Concurrent Programs

At a Glance

Hardcover

Shipping

How to return your order

Defective items

You Can Find This Book In

Other Editions and Formats

Paperback

More in Computer Science

Python Crash Course

3rd Edition - A Hands-On, Project-Based Introduction to Programming

The Tech Coup

How to Save Democracy from Silicon Valley

Nexus

A Brief History of Information Networks from the Stone Age to AI

The AI Con

How To Fight Big Tech's Hype and Create the Future We Want

The New Age of Sexism

How the AI Revolution is Reinventing Misogyny

Microsoft 365 Excel For Dummies

For Dummies (Computer/Tech)

Creative Machines

AI, Art & Us

Microsoft 365 Excel All-in-One For Dummies

Excel for Dummies

Empire of AI

Inside the reckless race for total domination

The AI-Driven Leader

Harnessing AI to Make Faster, Smarter Decisions

Python All-in-One For Dummies

3rd Edition

Artificial Intelligence and Human Rights, Democracy, and the Rule of Law

Computational Intelligence Techniques

Digital Daily Management

Transforming Data to Improvement

Transforming Cybersecurity with Machine Learning

Transforming Cybersecurity with Machine Learning

Application of Computational Techniques in Power Systems for Power Quality Improvement

Knowledge-based Engineering for Innovation

The Shortest History of AI

5G and Beyond Wireless Networks

Technology, Network Deployments, and Materials for Antenna Design

Advances in Digital Marketing in the Era of Artificial Intelligence

Case Studies and Data Analysis for Business Problem Solving

Advances on Mathematical Modeling and Optimization with Its Applications

Emerging Technologies

Array and Wearable Antennas

Design, Optimization, and Applications

Artificial Intelligence for Cyber Defense and Smart Policing

Artificial Intelligence of Things (AIoT)

New Standards, Technologies and Communication Systems

Autonomous Driving Network

Network Architecture in the Era of Autonomy

This product is categorised by