Handbook of Model Checking (eBook)

Edmund M. Clarke is Professor Emeritus in the Dept. of Computer Science at Carnegie Mellon University, where he was formerly the FORE Systems Professor. He received his Ph.D. in Computer Science from Cornell University in 1976. With E. Allen Emerson and Joseph Sifakis he received the ACM Turing Award in 2007 for his work on the development of model checking. He cofounded the Computer Aided Verification (CAV) conference, and the journal Formal Methods in Systems Design. Among many honors, he was elected to the US National Academy of Engineering and to the American Academy of Arts and Sciences. His research interests include software and hardware verification and automatic theorem proving.Thomas A. Henzinger is President of IST Austria (Institute of Science and Technology Austria). He holds a Ph.D. in Computer Science from Stanford University (1991). He has held assistant, associate, and full professorships in Cornell University (1992–95), the University of California, Berkeley (1996–2004), and EPFL in Lausanne, Switzerland (2004-09); he was also Director at the Max Planck Institute for Computer Science in Saarbrücken, Germany (1999). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. He is an ISI highly cited researcher, a member of Academia Europaea, the German Academy of Sciences (Leopoldina), and the Austrian Academy of Sciences, and a Fellow of the AAAS, ACM, and IEEE. He has received the Milner Award of the Royal Society, the Wittgenstein Award of the Austrian Science Fund, and an ERC Advanced Investigator Grant.Helmut Veith was a professor in the Faculty of Informatics of Technische Universität Wien, and an adjunct professor at Carnegie Mellon University. He received his PhD (sub auspiciis praesidentis) in Computer Science from TU Wien. He previously held professor positions at TU München and TU Darmstadt. In his research, he applied formal and logical methods to problems in software technology and engineering, focusing on model checking, software verification and testing, embedded software, and computer security. Prof. Veith passed away in 2016 during the final editing on the Handbook.Roderick Bloem received his PhD from the University of Colorado at Boulder (2001) for work on formal verification using linear temporal logic. He moved to Technische Universität Graz in 2002, where he has been a full professor since 2008. His research interests are in formal methods for the design and verification of digital systems, including hardware, software, and combinations such as embedded systems. He studies applications of game theory to the automatic synthesis of systems from their specifications, connections between temporal logics and omega-automata, model checking, and automatic fault localization and repair.

Handbook of Model Checking 3
Foreword 6
Preface 7
Acknowledgements 8
Contents 10
Contributors 18
Chapter 1: Introduction to Model Checking 22
1.1 The Case for Computer-Aided Veri?cation 22
1.2 Temporal-Logic Model Checking in a Nutshell 27
1.2.1 Kripke Structures 27
1.2.2 The Temporal Logic CTL 28
1.2.3 The Temporal Logic CTL 31
1.2.4 The Temporal Logic LTL 33
1.3 A Very Brief Guide Through the Chapters of the Handbook 34
1.3.1 The Algorithmic Challenge 36
1.3.2 The Modeling Challenge 39
1.4 The Future of Model Checking 40
References 43
Chapter 2: Temporal Logic and Fair Discrete Systems 48
2.1 Introduction 49
2.2 Fair Discrete Systems 50
2.2.1 Kripke Structures 51
2.2.2 De?nition of Fair Discrete System 51
2.2.3 Representing Programs 54
2.2.4 Algorithms 58
2.3 Linear Temporal Logic 62
2.3.1 De?nition of Linear Temporal Logic 63
2.3.2 Safety Versus Liveness and the Temporal Hierarchy 64
2.3.3 Extensions of LTL 67
2.3.4 Temporal Testers, Satis?ability, and Model Checking 71
2.4 Computation Tree Logic 73
2.4.1 De?nition of Computation Tree Logic 74
2.4.2 Extensions 75
2.4.3 Model Checking and Satis?ability 77
2.5 Examples for LTL and CTL 80
2.5.1 Invariance and Safety 81
2.5.2 Liveness 82
2.5.3 Additional Examples 83
2.6 CTL* 84
2.6.1 Branching vs. Linear Time 84
2.6.2 CTL* De?nition 88
2.6.3 Examples of Usage of CTL* 89
2.6.4 Model Checking and Satis?ability 90
References 91
Chapter 3: Modeling for Veri?cation 95
3.1 Introduction 95
3.2 Major Considerations in System Modeling 97
3.2.1 Selecting a Modeling Formalism and Language 98
3.2.1.1 Type of System 98
3.2.1.2 Type of Property 99
3.2.1.3 Modeling the Environment 99
3.2.1.4 Level of Abstraction 100
3.2.1.5 Clarity and Modularity 100
3.2.1.6 Form of Composition 101
3.2.1.7 Computational Engines 101
3.2.1.8 Practical Ease of Modeling and Expressiveness 102
3.2.2 Modeling Languages 102
3.2.3 Challenges in Modeling 103
3.2.4 Scope of This Chapter 105
3.3 Modeling Basics 106
3.3.1 Syntax 106
3.3.2 Dynamics 107
3.3.3 Modeling Concepts 108
3.4 Examples 109
3.4.1 Synchronous Circuits 110
3.4.1.1 Router Design 110
3.4.1.2 Simpli?cations and sml Model 111
3.4.1.3 Veri?cation Task: Progress Through the Router 111
3.4.1.4 Data Type Abstraction 113
3.4.1.5 Environment Modeling 114
3.4.1.6 Summary 116
3.4.2 Synchronous Control Systems 116
3.4.3 Concurrent Software 118
3.5 Kripke Structures 120
3.5.1 Transition Systems 121
3.5.2 From sml Programs to Kripke Structures 122
3.6 Summary 123
References 123
Chapter 4: Automata Theory and Model Checking 126
4.1 Introduction 126
4.2 Nondeterministic Büchi Automata on In?nite Words 127
4.2.1 De?nitions 127
4.2.2 Closure Properties 129
4.2.2.1 Closure Under Union and Intersection 129
4.2.2.2 Closure Under Complementation 131
4.2.3 Determinization 139
4.3 Additional Acceptance Conditions 141
4.3.1 Translations Among the Different Classes 143
4.3.1.1 Translations Among the Different Conditions 143
4.3.1.2 Typeness 143
4.3.1.3 Translations That Require a New State Space 145
4.3.2 Determinization of NBWs 149
4.4 Decision Procedures 151
4.5 Alternating Automata on In?nite Words 154
4.5.1 De?nition 155
4.5.2 Closure Properties 156
4.5.3 Decision Procedures 158
4.6 Automata-Based Algorithms 160
4.6.1 Translating LTL to Büchi Automata 161
4.6.1.1 A Translation via ABWs 161
4.6.1.2 A Direct Translation to NBWs 163
4.6.1.3 The Blow-up in the LTL to NBW Translation 164
4.6.2 Model Checking and Satis?ability 165
References 167
Chapter 5: Explicit-State Model Checking 171
5.1 Introduction 171
5.1.1 The Importance of Abstraction 172
5.2 Basic Search Algorithms 173
5.3 Linear Temporal Logic 176
5.4 Omega Automata 176
5.5 Nested Depth-First Search 178
5.6 Abstraction 180
5.6.1 Tic-Tac-Toe 181
5.7 Model-Driven Veri?cation 185
5.8 Incomplete Storage 186
5.8.1 Bitstate Hashing and Bloom Filters 186
5.9 Extensions 187
5.10 Synopsis 188
References 188
Chapter 6: Partial-Order Reduction 190
6.1 Introduction 190
6.2 Partial Order Reduction 191
Reduction for LTL 193
On-the-Fly Model Checking 197
Reduction for CTL 198
Reduction for Process Algebra 199
Reducing Visibility 199
6.3 Reducing Edges While Preserving States 199
Sleep Sets 200
Trace Normal Form 201
Edge Lean Algorithm 204
6.4 Conclusions 205
References 205
Chapter 7: Binary Decision Diagrams 208
7.1 Introduction 208
7.2 Terminology 209
7.3 A Boolean Function API 210
7.4 OBDD Representation 212
7.5 Implementing OBDD Operations 214
7.6 Implementation Techniques 217
7.7 Variable Ordering and Reordering 219
7.8 Variant Representations 220
7.9 Representing Non-Boolean Functions 223
7.10 Scaling OBDD Capacity 227
Comparison to SAT Checking 229
7.11 Concluding Remarks 230
References 231
Chapter 8: BDD-Based Symbolic Model Checking 235
8.1 Introduction 235
8.2 Preliminaries 236
8.3 Binary Decision Diagrams: The Basics 238
8.3.1 Representing Sets and Relations 238
8.3.1.1 Characteristic Function 238
8.3.1.2 Representing Sets 239
8.3.1.3 Representing Relations 240
8.3.2 Image Computation 240
8.3.3 Partitioned Transition Relation 242
8.3.3.1 Disjunctive Decomposition 242
8.3.3.2 Conjunctive Decomposition 243
8.3.4 Historical Perspective 244
8.4 Model Checking Kripke Structures 246
8.4.1 Reachability/Invariant/AG 247
8.4.2 CTL Model Checking 247
8.4.3 Fair CTL Model Checking 249
8.4.3.1 Function egFairStates 250
8.4.3.2 Function ctlFairStates 251
8.4.4 LTL Model Checking 251
8.4.4.1 Restricted Path Formula 252
8.4.4.2 Algorithm ltlTableau 253
8.5 Push-Down Symbolic Model Checking 254
8.6 Conclusion 259
References 260
Chapter 9: Propositional SAT Solving 262
9.1 Introduction 262
9.2 Preliminaries 264
9.3 CDCL SAT Solvers: Organization 267
9.4 CDCL SAT Solvers 268
9.4.1 Clause Learning and Non-chronological Backtracking 269
9.4.2 Unique Implication Points 271
9.4.3 Learned Clause Minimization 274
9.4.4 Lazy Data Structures 276
9.4.5 Search Restarts 278
9.4.6 Lightweight Branching Heuristics 278
9.4.7 Additional Techniques and Recent Trends 279
9.5 SAT-Based Problem Solving 279
9.5.1 Incremental SAT 280
9.5.2 Unsatis?able Cores 280
9.5.3 CNF Encodings 281
9.5.4 Optimization 282
9.5.5 Model Enumeration 282
9.5.6 Minimal Sets 283
9.5.7 Quanti?cation 283
9.6 Research Directions 284
References 284
Chapter 10: SAT-Based Model Checking 291
10.1 Introduction 291
10.2 Bounded Model Checking on Kripke Structures 292
10.2.1 Kripke Structures 292
10.2.2 Safety Properties 293
10.2.3 Liveness Properties 294
10.2.3.1 Liveness to Safety Translation 295
10.2.3.2 k-Liveness 295
10.3 Bounded Model Checking for Hardware Designs 295
10.3.1 Hardware Description Languages (HDLs) 296
10.3.2 BMC on Net-Lists 296
10.4 Bounded Model Checking for Software 297
10.4.1 Monolithic Encodings 298
10.4.2 Path-Based Encodings 298
10.4.3 Completeness for Bounded Programs 299
10.4.4 BMC for Multi-threaded Programs 300
10.4.5 Bounded Model Checking for HW/SW Co-veri?cation 300
10.5 Encodings into Propositional SAT 301
10.5.1 Encoding Bit Vectors 301
10.5.2 Encoding Memory 302
10.5.3 Encodings with Under- and Over-approximation 302
10.6 Complete Model Checking with SAT 303
10.6.1 Completeness Thresholds 303
10.6.2 Image Computation with SAT 303
10.6.3 Basic Inductive Techniques 304
10.6.3.1 Strengthening the Inductive Argument 304
10.6.3.2 Equivalence Reasoning 304
10.6.3.3 Temporal Decomposition 305
10.6.3.4 k-Induction 305
10.6.4 Craig Interpolation 305
10.6.5 Iterative Inductive Strengthening 306
10.7 Abstraction Techniques Using SAT 306
10.7.1 Overview of Predicate Abstraction 306
10.7.2 Computing Abstractions with SAT 307
10.7.3 Simulation with SAT 308
10.7.4 Abstraction-Based Tools 308
10.8 Outlook and Conclusions 309
References 309
Chapter 11: Satis?ability Modulo Theories 318
11.1 Introduction 318
11.1.1 Technical Preliminaries 320
11.2 SMT in Model Checking 323
11.3 The Lazy Approach to SMT 325
11.3.1 A Basic Lazy SMT Solver 326
11.3.2 SAT Engine and Theory Solver Features 326
11.3.3 A General Framework and Architecture 328
11.4 Theory Solvers for Speci?c Theories 330
11.4.1 Uninterpreted Function Symbols 330
11.4.2 Real Arithmetic 331
11.4.3 Integer Arithmetic 332
11.4.4 Mixed Integer and Real Arithmetic 334
11.4.5 Difference Logic 334
11.4.6 Bit Vectors 335
11.4.7 Arrays 336
11.4.8 Other Theories 337
11.5 Combining Theory Solvers 337
11.5.1 A Basic Combination Method 338
11.5.2 Combination Variants and Extensions 339
11.6 SMT Solving Extensions and Enhancements 340
11.7 Eager Encodings to SAT 343
11.8 Additional Functionalities of SMT Solvers 345
References 348
Chapter 12: Compositional Reasoning 357
12.1 Introduction 357
12.2 Reasoning with Assertions 360
12.2.1 The (Non-compositional) Owicki-Gries Method 360
12.2.2 The Assume-Guarantee View: Localized Inductive Invariants 361
12.2.2.1 The Shared-Variable Program Model 362
A Note on Notation 362
Invariant Assertions 362
12.2.2.2 Split Invariants 363
12.2.3 Computing the Strongest Split Invariant 364
Split Invariance for N Processes 365
12.2.4 Relationship to Rely-Guarantee 366
12.2.5 Completeness Issues 366
12.2.6 Deadlock Detection with Local Invariants 368
12.2.7 Local Proofs for Termination, Temporal Properties, and Fairness 368
12.2.7.1 Background 368
12.2.7.2 Local Proof Rules for Liveness Properties 369
12.2.8 Algorithms for Local Analysis of Temporal Properties 370
12.2.9 Automating the Discovery of Auxiliary Variables 371
12.2.10 Local Symmetry 373
12.2.11 Further Reading 374
12.3 Automata-Based Assume-Guarantee Reasoning 374
12.3.1 Formalisms 374
12.3.1.1 Finite-State Machines 374
12.3.1.2 Parallel Composition of FSMs 375
12.3.1.3 Properties 375
12.3.1.4 Complementation 376
12.3.2 Assume-Guarantee Reasoning 376
12.3.2.1 Assume-Guarantee Triples 376
12.3.2.2 Weakest Assumption 376
12.3.2.3 Basic Assume-Guarantee Rule 377
Rule ASym 377
12.3.2.4 Soundness and Completeness 377
12.3.3 Automation of Basic Assume-Guarantee Rule 378
12.3.3.1 The L* algorithm 378
12.3.3.2 Learning-Based Assumption Generation 379
12.3.3.3 Correctness Arguments 381
12.3.4 Example 381
12.3.5 Additional Assume-Guarantee Rules and Their Automation 384
Rule ASymN 384
Rule Circ-0 385
Rule Sym 385
Rule SymN 386
Rule Circ 386
Rule Circ-Ind 386
12.4 Related Approaches 387
12.4.1 Learning for Compositional Veri?cation 387
12.4.2 Assumption Generation by Abstraction-Re?nement 387
12.4.3 Components and Interfaces 388
12.4.4 Other Modular Reasoning Frameworks 389
12.5 Conclusion 390
References 390
Chapter 13: Abstraction and Abstraction Re?nement 396
13.1 Introduction 396
13.2 Preliminaries 398
13.2.1 Abstraction Frameworks 398
13.2.2 Kripke Structures 399
13.2.3 The µ-Calculus 401
13.2.3.1 Some Notes on the Difference Between Lµ and CTL/CTL* 403
13.3 Simulation and Bisimulation Relations 405
13.3.1 Simulation Relation 405
13.3.2 Bisimulation Relation 407
13.3.3 Additional Reading 409
13.4 Abstraction Based on Simulation 410
13.4.1 Existential Abstraction 410
13.4.1.1 Speci?c Abstractions: Examples 412
13.4.2 Additional Reading 413
13.5 CounterExample-Guided Abstraction Re?nement (CEGAR) 413
13.5.1 The CEGAR Framework 415
13.5.1.1 Identifying Spurious Path Counterexamples 415
13.5.2 Additional Reading 417
13.6 Abstraction Based on Modal Simulation 417
13.6.1 A Three-Valued Setting 420
13.6.2 Re?nement 422
13.6.3 Additional Reading 422
13.7 Completeness 423
13.7.1 Additional Reading 424
References 425
Chapter 14: Interpolation and Model Checking 431
14.1 Introduction 431
14.2 Preliminaries 433
14.3 Model of Abstraction Re?nement 434
14.3.1 A Simple Programming Language and Proof System 435
14.3.2 The Abstractor 436
14.3.3 The Re?ner 438
14.4 Re?nement, Local Proofs, and Interpolants 438
14.4.1 Craig Interpolation 439
14.4.2 Feasible Interpolation in Model Checking 441
14.4.3 Interpolants and Local Proofs 441
14.5 Re?ners as Local Proof Systems 444
14.5.1 Strongest Post-condition 444
14.5.2 Weakest Pre-condition 447
14.5.3 Bounded Provers 448
14.5.4 Split Provers and Language Strati?cation 449
14.5.5 Constraint-Based Interpolation 450
14.5.6 Feasible Interpolation and Re?nement 450
14.5.7 Improving Interpolants 451
14.6 Abstractors as Proof Generalizers 451
14.7 Summary 453
References 454
Chapter 15: Predicate Abstraction for Program Veri?cation 457
15.1 Introduction 457
15.2 De?nitions 458
15.2.1 Programs 458
15.2.2 Correctness: Safety and Termination 461
15.3 Characterizing Correctness via Reachability 462
15.3.1 Safety and Reachability 462
15.3.2 Termination and Binary Reachability 463
15.4 Characterizing Correctness via Inductiveness 464
15.4.1 Safety and Closure Under post 464
15.4.2 Termination and Transitive Closure 467
15.5 Abstraction 469
15.5.1 Safety and Predicate Abstraction 470
15.5.2 Termination and Transition Predicate Abstraction 476
15.6 Abstraction Re?nement 481
15.6.1 Re?nement of Predicate Abstraction 482
15.6.2 Re?nement of Transition Predicate Abstraction 488
15.7 Solving Re?nement Constraints for Predicate Abstraction 491
15.7.1 Least Solution 492
15.7.2 Greatest Solution 493
15.7.3 Intermediate Solution Using Interpolation 495
15.8 Tools 496
15.9 Conclusion 497
References 497
Chapter 16: Combining Model Checking and Data-Flow Analysis 502
16.1 Introduction 503
16.2 General Considerations 503
16.2.1 Type Checking 503
16.2.2 Data-Flow Analysis 505
16.2.3 Model Checking 508
16.3 Unifying Formal Framework/Comparison of Algorithms 510
16.3.1 Preliminaries 510
16.3.2 Algorithm of Data-Flow Analysis 513
16.3.3 Algorithm of Model Checking 515
16.3.4 Uni?ed Algorithm Using Con?gurable Program Analysis 515
16.3.5 Discussion 518
16.3.6 Composition of Con?gurable Program Analyses 519
16.4 Classic Examples (Component Analyses) 520
16.4.1 Reachable-Code Analysis 520
16.4.2 Constant Propagation 521
16.4.3 Reaching De?nitions 522
16.4.4 Predicate Analysis 524
16.4.5 Explicit-Heap Analysis 525
16.4.6 BDD Analysis 526
16.4.7 Observer Automata 527
16.5 Combination Examples (Composite Analyses) 529
16.5.1 Predicate Analysis + Constant Propagation 529
16.5.2 Predicate Analysis + Constant Propagation + Strengthen 530
16.5.3 Predicate Analysis + Explicit-Heap Analysis 532
16.5.4 Predicate Analysis + Observer Automata 532
16.6 Algorithms for Constructing Program Invariants 534
16.6.1 Iterative and Monotonic Fixed-Point Approaches 534
16.6.2 Counterexample-Guided Abstraction Re?nement 535
16.6.3 Template- and Constraint-Based Approaches 536
16.6.4 Proof-Rule-Based Approaches 537
16.6.5 Iterative, but Non-monotonic Approaches 537
16.6.6 Comparison with Standard Recurrence Solving 538
16.6.7 Discussion 540
16.7 Combinations in Tool Implementations 541
16.8 Conclusion 541
References 543
Chapter 17: Model Checking Procedural Programs 550
17.1 Introduction 550
17.2 Models of Procedural Programs 552
17.2.1 (Extended) Recursive State Machines 553
17.2.2 Pushdown Systems 554
17.2.3 From RSMs to PDSs 555
17.3 Basic Veri?cation Algorithms 556
17.3.1 The State Reachability Problem: Computing Summaries 556
17.3.2 The Fair Computation Problem 559
17.3.3 The Con?guration Reachability Problem: Saturating Automata 560
17.3.3.1 Computing pre*(C) for a Regular Set C by Saturation 561
17.3.3.2 Computing post*(C) for a Regular Set C by Saturation 562
17.3.4 The Generalized Fair Computation Problem 564
17.4 Specifying Requirements 565
17.4.1 Nested Words 566
17.4.2 Nested Word Automata 567
17.4.2.1 RSMs as NWAs 568
17.4.2.2 NWAs for Requirements 569
17.4.2.3 Closure Properties 570
17.4.2.4 Decision Problems 570
17.4.2.5 MSO Equivalence 571
17.4.3 Temporal Logics 571
17.4.3.1 Abstract Next 572
17.4.3.2 Abstract Paths 573
17.4.3.3 Summary Paths 573
17.4.3.4 Model Checking 574
17.5 Bibliographical Remarks 575
17.5.1 Summarization 575
17.5.2 Saturation 576
17.5.3 Temporal Logic Model Checking 577
References 578
Chapter 18: Model Checking Concurrent Programs 582
18.1 Introduction 583
18.2 Concurrent System Model and Notation 585
18.2.1 Synchronization and Communication 587
18.2.2 Speci?cation Logic 587
18.2.3 Interacting Pushdown System (PDS) Model 588
18.3 PDS-Based Model Checking: Synchronization Patterns 589
18.3.1 Programs with Nested Locks 590
18.3.1.1 Pair-wise Reachability for Nested Locks 590
18.3.1.2 Model-Checking Programs with Nested Locks 591
18.3.2 Programs with Locks: Lock Causality Graph 595
18.3.3 Programs with Bounded Lock Chains 597
18.3.4 Discussion: Lock Patterns 600
18.3.5 Programs with Rendezvous 601
18.3.5.1 Computing Over-approximations of Path Languages 602
18.3.5.2 De?ning Re?nable Finite-Chain Abstractions 603
18.3.5.3 Checking Whether the Counterexample Is Spurious 604
18.3.5.4 The Semi-decision Procedure 604
18.4 PDS-Based Model-Checking: Communication Patterns 604
18.4.1 Reasoning About Programs with State Observation 605
18.4.1.1 Symbolic Representation of PDN Con?gurations 605
18.4.1.2 Reachability Analysis of PDNs 606
18.4.2 Multiphase Acyclic Pushdown Networks 606
18.4.2.1 The Reachability Problem for MAPNs 607
18.4.2.2 For MAPNs 608
18.4.2.3 A Semi-algorithm for k-Bounded Reachability for MAPNs 609
18.4.2.4 A Semi-algorithm for the Reachability Problem for General PDNs 610
18.4.3 Threads Communicating via Lossy Channels 610
18.5 Other Models: Finite State Systems and Sequential Programs 611
18.5.1 Partial-Order Reduction 612
18.5.2 Symbolic Reasoning with Memory Consistency Constraints 613
18.5.3 Concurrent Data?ow Analysis and Invariant Generation 614
18.5.4 Trace-Based Dynamic Model-Checking 615
18.5.5 Other Related Techniques 616
References 616
Chapter 19: Combining Model Checking and Testing 621
19.1 Introduction 621
19.2 Systematic Testing of Concurrent Software 623
19.2.1 Classical Model Checking 623
19.2.2 Software Model Checking Using a Dynamic Semantics 623
19.2.3 Systematic Testing with a Run-Time Scheduler 627
19.2.4 Stateless vs. Stateful Search 628
19.2.5 Systematic Testing for Multi-threaded Programs 629
19.2.6 Tools and Applications 631
19.3 Systematic Testing of Sequential Software 632
19.3.1 Classical Symbolic Execution 632
19.3.2 Static Test Generation 633
19.3.3 Dynamic Test Generation 634
19.3.4 Systematic Dynamic Test Generation 635
19.3.5 Strengths and Limitations 639
19.3.6 Tools and Applications 640
19.4 Systematic Testing of Concurrent Software with Data Inputs 641
19.4.1 Example 642
19.4.2 Comparison with Related Work 643
19.5 Other Related Work 645
19.6 Conclusion 648
References 648
Chapter 20: Combining Model Checking and Deduction 658
20.1 Introduction 658
20.2 Logic Background 663
20.2.1 Propositional Logic 663
20.2.2 First-Order Logic 668
20.2.3 Higher-Order Logic 672
20.2.4 PVS: Computation and Deduction 673
20.2.5 Hoare Logic 674
20.3 Deduction and Model Checking 677
20.3.1 Abstract Interpretation 677
20.3.2 Symbolic Model Checking 679
20.3.3 Predicate Abstraction 680
20.3.4 Bounded Model Checking and k-Induction 682
20.3.5 Symbolic Execution and Test Generation 683
20.3.6 Interpolation-Based Model Checking 684
20.3.7 Con?ict-Directed Reachability 685
20.4 Conclusions 687
References 687
Chapter 21: Model Checking Parameterized Systems 692
21.1 Introduction 692
21.2 Petri Nets 694
21.2.1 Simple Protocol 694
21.2.2 Petri Nets 695
21.2.3 Safety Properties 697
21.2.4 Backward Reachability Analysis 698
21.2.5 Liveness Properties 701
21.3 Regular Model Checking 702
21.3.1 Near-Neighbor Communication 702
21.3.2 Regular Model Checking 703
21.3.3 Acceleration Techniques 705
Safety Properties 705
Column Transducer 706
Quotienting 707
Example 709
21.4 Monotonic Abstraction 710
21.4.1 Example 711
21.4.2 Model 712
21.4.3 Over-Approximation 713
21.4.4 Backward Reachability Algorithm 714
21.5 Compositional Reasoning for Parameterized Veri?cation 716
21.5.1 Parameterized Protocols 716
Index Variables 717
States 717
Expressions 717
Assignments 717
Rules 718
Protocols 718
Safety Properties 718
21.5.2 The CMP Method 719
21.5.2.1 German's Protocol 720
21.5.2.2 Abstraction 720
21.5.2.3 Strengthening 722
21.5.2.4 Correctness 723
21.5.3 Evolution of the CMP Method 725
21.5.4 Applications 725
21.6 Related Work 726
References 728
Chapter 22: Model Checking Security Protocols 733
22.1 Introduction 733
22.2 History 737
22.3 Formal Model 739
22.3.1 Notational Preliminaries 740
22.3.2 Terms and Events 740
22.3.3 Protocols and Threads 742
22.3.4 Initial Adversary Knowledge 743
22.3.5 Execution Model 743
22.3.6 Property Speci?cation 745
22.3.7 Alternatives 746
22.4 Issues in Developing Model-Checking Algorithms for Security Protocols 747
22.4.1 Forward Versus Backward Search 747
22.4.2 Bounded Instances 748
22.4.3 Representing States 749
22.4.4 Partial-Order Reduction 751
22.4.5 Handling Equations 752
22.5 Systems and Algorithms 754
22.5.1 NPA and Maude-NPA 754
22.5.2 AVISPA and Related Tools 755
22.5.3 Athena, Scyther, and Tamarin 757
22.5.4 ProVerif 758
22.6 Research Problems 759
22.6.1 Link to Computational Soundness 759
22.6.2 Corruption Models 760
22.6.3 Channel Properties 761
22.6.4 Other Properties, Including Non-trace Properties 761
22.6.5 Probabilities 762
22.7 Conclusions 763
References 764
Chapter 23: Transfer of Model Checking to Industrial Practice 769
23.1 Introduction 769
23.1.1 Anything Worth Inventing Is Worth Reinventing 770
23.1.2 The Interplay Between Theory and Application 772
23.2 The Technology Transfer Problem 773
23.2.1 Initial Challenges 773
23.2.2 Barriers to Technology Transfer 774
23.2.3 Methodological Differences and New Potential Bene?ts 775
23.2.4 The Cost of Writing Properties vs. a Test Bench 776
23.2.5 Settling on a Scope for Model Checking 777
23.2.6 The First Commercial Successes 779
23.2.7 The Essentiality of Being Able to Compare Tools 780
23.2.8 In Summary 781
23.3 False Starts 782
23.4 A Framework for Technology Transfer 785
23.5 Formal Functional Veri?cation in Commercial Use Today 788
23.6 Algorithms 792
23.7 Future 794
23.8 Conclusion 795
References 796
Chapter 24: Functional Speci?cation of Hardware via Temporal Logic 800
24.1 Introduction 800
24.2 From LTL to Regular-Expression-Based Temporal Logic 802
24.2.1 Adding Expressive Power-Suf?x Implication 803
24.2.2 Adding Succinctness 804
24.2.2.1 Counting 804
24.2.2.2 First Match 805
24.2.2.3 Intersection 805
24.2.2.4 Fusion 806
24.2.2.5 Past Operators 807
24.2.3 Distinguishing Between Weak and Strong Regular Expressions 807
24.3 Clocks and Sampling 810
24.3.1 Hardware Clocks 810
24.3.2 Using a Clock as a Time-Sampling Abstraction 814
24.4 Hardware Resets and Other Sources of Truncated Paths 814
24.4.1 Hardware Resets 815
24.4.2 Other Sources of Truncated Paths 817
24.4.3 The Truncated Semantics and Classi?cation of Safety Formulas 820
24.5 The Simple Subset 822
24.6 Quanti?ed and Local Variables 823
24.6.1 Quanti?ed Variables 823
24.6.2 Local Variables 824
24.7 Summary and Open Issues 828
24.7.1 One-to-One Correspondence 828
24.7.2 Triggering Procedural Code from Within a Formula 829
24.7.3 Separation of Concerns 829
References 830
Chapter 25: Symbolic Trajectory Evaluation 835
25.1 Introduction 835
25.2 Notational Preliminaries 837
25.3 Sequential Circuit Models in STE 838
25.3.1 States and Sequences 838
25.3.2 Abstraction 839
25.3.3 Time-Dependent Behaviour 840
25.3.4 The Next State Function and Trajectories 841
25.4 Trajectory Evaluation Logic 842
25.4.1 Correctness Properties for Veri?cation 844
25.4.2 Correctness Properties Under Assumptions 846
25.4.3 Internal Combinational Circuitry 846
25.5 The Fundamental Theorem of Trajectory Evaluation 847
25.6 STE Model Checking 848
25.6.1 The Symbolic Model-Checking Algorithm 850
25.6.2 Some Small Examples in Detail 852
25.6.3 Model Checking Properties Under Assumptions 854
25.7 Abstraction and Symbolic Indexing 856
25.7.1 Symbolic Indexing 857
25.8 Compositional Reasoning 861
25.8.1 The STE Deductive System 862
25.8.2 Relational STE 864
25.9 GSTE and Other Extensions 866
25.9.1 Generalized Symbolic Trajectory Evaluation 868
25.10 Summary and Prospects 869
References 871
Chapter 26: The mu-calculus and Model Checking 875
26.1 Introduction 875
26.2 Basics 876
26.2.1 Syntax and Semantics 876
26.2.2 Alternation Depth 882
26.2.3 Semantics in Terms of Games 884
26.2.3.1 Games 886
26.2.3.2 Veri?cation Game 887
26.2.4 Model Checking 891
26.3 Fundamental Properties 894
26.3.1 Bisimulation Invariance and the Tree-Model Property 895
26.3.2 Modal Automata 896
26.3.3 Satis?ability 900
26.3.4 Alternation Hierarchy 903
26.3.5 Proof System 905
26.3.6 Interpolation Property 905
26.3.7 Division Property 906
26.4 Relations with Other Logics 908
26.4.1 MSOL, Binary Trees and Bisimulation Invariance 908
26.4.2 Embedding of Program Logics 910
26.4.3 Beyond µ-Calculus 912
26.4.3.1 Iterated Structures 912
26.4.3.2 Guarded Logics 914
26.5 Related Work 916
References 918
Chapter 27: Graph Games and Reactive Synthesis 924
27.1 Introduction 924
27.2 Theory of Graph-Based Games 926
27.2.1 Game Graphs and Strategies 927
27.2.2 Objectives 928
27.2.3 Winning and Optimal Strategies Decision Problems
27.2.4 Complexity and Algorithms for Graph Games with Qualitative Objectives 930
27.2.5 Complexity and Algorithms for Graph Games with Quantitative Objectives 935
27.2.6 Reducibility Between Graph Games 937
27.2.7 Extensions 937
27.3 Reactive Synthesis 939
27.3.1 Introduction 939
27.3.2 Games, Transducers, Trees, and Automata 941
27.3.3 Realizability and Synthesis Problem 945
27.3.4 Classical Approach to LTL Synthesis 946
Step 1: LTL to NBW 946
Step 2: NBW to DPW 946
Step 3: DPW to DPT 947
Step 4: DPT Emptiness Check 947
Step 5: Construction of Finite-State Transducer 948
27.3.5 Recent Approaches to LTL Synthesis 949
27.3.5.1 Bounded (or Safraless) Approaches 949
Step 1: LTL to UCT 950
Step 2: UCT to k-UCT 951
Step 3: k-UCT Emptiness Check 952
Step 4: System Construction 954
27.3.5.2 Approaches for Fragments of LTL 954
27.4 Related Topics 956
References 957
Chapter 28: Model Checking Probabilistic Systems 966
28.1 Introduction 967
28.1.1 Temporal Logics for Specifying Probabilistic Properties 967
28.1.2 Model-Checking Algorithms for Probabilistic Systems 969
28.1.3 Outline 969
28.2 Modelling Probabilistic Concurrent Systems 969
28.2.1 Preliminaries 970
28.2.2 Markov Decision Processes 970
28.2.3 Markov Chains 973
28.2.4 Schedulers 973
28.2.5 Probability Measures in MDPs 974
28.2.6 Maximal and Minimal Probabilities for Path Events 975
28.2.7 Maximal and Minimal Expected Cost 976
28.3 Probabilistic Computation Tree Logic 978
28.3.1 Syntax of PCTL 978
28.3.2 Semantics of PCTL 979
28.3.3 Derived Operators 981
28.4 Model-Checking Algorithms for MDPs and PCTL 983
28.4.1 Probability Operator 983
28.4.2 Expectation Operator 986
28.5 Linear Temporal Logic 988
28.5.1 Syntax of LTL 988
28.5.2 Semantics of LTL 989
28.5.3 Derived Operators 989
28.5.4 LTL Model-Checking Problem 989
28.6 Model-Checking Algorithms for MDPs and LTL 990
28.7 Tools, Applications and Model Construction 993
28.7.1 Tool Support 993
28.7.2 Applications 994
28.7.3 Construction of Probabilistic Models 994
28.8 Extensions of the Model and Speci?cation Notations 995
28.9 Conclusion 996
References 996
Chapter 29: Model Checking Real-Time Systems 1003
29.1 Introduction 1003
29.2 Timed Automata 1005
29.3 Checking Reachability 1009
29.3.1 Region Equivalence 1009
29.3.2 Some Extensions of Timed Automata 1010
29.4 (Bi)simulation Checking 1012
29.4.1 (Bi)simulations for Timed Automata 1012
29.4.2 Checking (Bi)simulations 1013
29.5 Language-Theoretic Properties 1014
29.5.1 Language of a Timed Automaton 1014
29.5.2 Timed Automata with epsilon-Transitions 1014
29.5.3 Clock Constraints as Acceptance Conditions 1015
29.5.4 Intersection, Union, and Complement 1016
29.5.5 Language Emptiness, Inclusion 1017
29.6 Timed Temporal Logics 1020
29.6.1 Linear-Time Temporal Logics 1020
Continuous Semantics 1020
Pointwise Semantics 1021
29.6.2 Veri?cation of Linear-Time Temporal Logics 1021
29.6.3 Branching-Time Temporal Logics 1023
29.6.4 Veri?cation of Branching-Time Temporal Logics 1024
29.7 Symbolic Algorithms, Data Structures, Tools 1025
29.7.1 Zones and Operations 1025
29.7.2 Symbolic Datastructures 1026
29.7.3 Practical Ef?ciency 1028
29.7.4 Tools and Applications 1029
29.8 Weighted Timed Automata 1030
29.8.1 Cost-Optimal Schedules 1031
29.8.2 Weighted Temporal Logics 1033
29.8.3 Energy Constraints 1034
29.9 Timed Games 1036
29.10 Ongoing and Future Challenges 1039
References 1039
Chapter 30: Veri?cation of Hybrid Systems 1049
30.1 Introduction 1050
30.2 Basic De?nitions 1051
30.2.1 Predicates 1052
30.2.2 Hybrid Automata 1054
30.3 Decidability and Undecidability Results 1057
30.4 Set-Based Reachability Analysis 1060
30.4.1 Reachability Algorithm 1060
30.4.2 Piecewise Constant Dynamics 1062
30.4.3 Piecewise Af?ne Dynamics 1066
30.4.3.1 Successor Computations 1067
30.4.3.2 Set Representations 1072
30.4.3.3 Clustering 1076
30.4.4 Nonlinear Dynamics 1076
30.5 Abstraction-Based Veri?cation 1077
30.5.1 Discrete Abstractions 1078
30.5.2 Phase-Portrait Approximation 1080
30.5.3 Predicate Abstractions 1081
30.5.4 Abstraction Re?nement 1084
30.5.5 Approximate Bisimulations 1085
30.6 Logic-Based Veri?cation 1086
30.6.1 Polynomial Barrier Certi?cates 1089
30.6.2 Equational Certi?cates 1091
30.6.3 Differential Invariants and Logical Certi?cates 1092
30.7 Veri?cation Tools 1099
HSolver: Interval Constraint Propagation 1100
HyTech: The HYbrid TECHnology Tool 1100
KeYmaera: Logic and Differential Invariants for Compositional Veri?cation 1101
PHAVer: Polyhedral Hybrid Automaton Verifyer 1102
SpaceEx: State Space Explorer 1103
ToolboxLS: Level Set Methods 1103
References 1104
Chapter 31: Symbolic Model Checking in Non-Boolean Domains 1113
31.1 Introduction 1113
31.2 Transition Systems and Symbolic Veri?cation 1114
31.2.1 Systems: Transition Systems 1114
31.2.2 Properties and Algorithms: The µ-Calculus 1115
31.2.3 Symbolic Model Checking 1117
31.2.4 Examples of Properties and Their Veri?cation Algorithms 1118
31.2.5 Equivalence Relations and Termination 1120
31.3 Examples of Symbolic Veri?cation 1121
31.3.1 Program Veri?cation 1121
31.3.2 Antichain-Based Algorithms for Finite-State Automata 1123
31.3.3 Timed and Hybrid Systems 1126
31.3.4 Well-Structured Transition Systems 1130
31.4 Games and Symbolic Synthesis 1133
31.4.1 Deterministic Games 1133
31.4.2 The Boolean µ-Calculus on Games 1134
31.4.3 Linear-Time Properties 1135
31.4.4 From Veri?cation to Synthesis 1137
31.4.5 Examples of Synthesis 1138
31.5 Probabilistic Systems 1139
31.5.1 Probabilistic Games and Objectives 1140
31.5.2 The Quantitative µ-calculus 1141
31.6 Conclusion 1143
References 1145
Chapter 32: Process Algebra and Model Checking 1150
32.1 Introduction 1150
32.2 Foundations 1151
32.2.1 CCS: Process Algebra via Operational Semantics 1152
32.2.1.1 Syntax of CCS 1152
Actions in CCS 1152
CCS Operators 1153
32.2.1.2 The Operational Semantics of CCS 1154
32.2.1.3 CCS and Labeled Transition Systems 1155
32.2.1.4 Bisimulation 1156
32.2.1.5 A Logical Characterization of Bisimilarity 1158
Syntax of HML 1158
Semantics of HML 1159
Bisimulation vis-à-vis HML 1159
32.2.1.6 Observational Equivalence and Congruence for CCS 1160
32.2.1.7 Axiomatizations of Bisimilarity and Observational Congruence 1162
Inference Rules for Equational Reasoning 1162
Axiomatizing Bisimilarity 1163
Axiomatizing Observational Congruence 1164
Axiomatizing Full CCS 1164
32.2.2 CSP: Process Algebra via Denotational Semantics 1164
32.2.2.1 CSP Syntax 1165
Actions in CSP 1165
CSP Constructs 1166
32.2.2.2 Models for CSP Processes 1168
32.2.2.3 A Denotational Semantics for CSP 1171
32.2.2.4 Timed CSP 1173
32.2.3 ACP: Process Algebra via Equational Semantics 1173
32.2.3.1 BPA 1173
32.2.3.2 PA 1174
32.2.3.3 ACP 1175
32.3 Algorithms and Methodologies 1176
32.3.1 Bisimulation and Simulation 1176
32.3.2 Checking Re?nement over Behavioral Models 1178
32.3.3 Diagnostic Information (HML , FD) 1179
32.3.4 Compositional Veri?cation 1181
32.4 Tools 1182
32.4.1 FDR 1182
32.4.1.1 Using FDR 1183
32.4.2 The Concurrency Workbench 1184
32.4.3 XMC 1185
32.4.4 mCRL2 1185
32.5 Case Studies 1186
32.5.1 Distributed Leadership Election (FDR) 1186
32.5.2 Active-Structure Control System (CWB) 1189
32.5.3 GNU i-Protocol (XSB) 1190
32.6 Conclusions 1191
References 1192
Index 1197