Scalable Techniques for Formal Verification (eBook)

Scalable Techniques for Formal Verification 1
Preface 7
Contents 11
1 Introduction 15
Part I Preliminaries 20
2 Overview of Formal Verification 21
2.1 Theorem Proving 21
2.2 Temporal Logic and Model Checking 24
2.3 Program Logics, Axiomatic Semantics, and Verification Conditions 29
2.4 Bibliographic Notes 34
3 Introduction to ACL2 36
3.1 Basic Logic of ACL2 36
3.2 Ground Zero Theory 38
3.2.1 Terms, Formulas, Functions, and Predicates 41
3.2.2 Ordinals and Well-Founded Induction 43
3.3 Extension Principles 46
3.3.1 Definitional Principle 47
3.3.2 Encapsulation Principle 51
3.3.3 Defchoose Principle 53
3.4 The Theorem Prover 55
3.5 Structuring Mechanisms 56
3.6 Evaluators 57
3.7 The ACL2 Programming Environment 58
3.8 Bibliographic Notes 59
Part II Sequential Program Verification 61
4 Sequential Programs 62
4.1 Modeling Sequential Programs 62
4.2 Proof Styles 64
4.2.1 Stepwise Invariants 64
4.2.2 Clock Functions 65
4.3 Comparison of Proof Styles 66
4.4 Verifying Program Components and Generalized Proof Obligations 68
4.5 Discussion 71
4.5.1 Overspecification 71
4.5.2 Forced Homogeneity 72
4.6 Summary 73
4.7 Bibliographic Notes 73
5 Operational Semantics and Assertional Reasoning 74
5.1 Cutpoints, Assertions, and VCG Guarantees 74
5.2 VCG Guarantees and Symbolic Simulation 77
5.3 Composing Correctness Statements 79
5.4 Applications 81
5.4.1 Fibonacci Implementation on TINY 82
5.4.2 Recursive Factorial Implementation on the JVM 84
5.4.3 CBC-Mode Encryption and Decryption 84
5.5 Comparison with Related Approaches 85
5.6 Summary 87
5.7 Bibliographic Notes 87
6 Connecting Different Proof Styles 89
6.1 Soundness of Proof Styles 90
6.2 Completeness 92
6.3 Remarks on Mechanization 96
6.4 Discussion 96
6.5 Summary and Conclusion 98
6.6 Bibliographic Notes 99
Part III Verification of Reactive Systems 101
7 Reactive Systems 102
7.1 Modeling Reactive Systems 103
7.2 Stuttering Trace Containment 104
7.3 Fairness Constraints 106
7.4 Discussion 110
7.5 Summary 113
7.6 Bibliographic Notes 114
8 Verifying Concurrent Protocols Using Refinements 115
8.1 Reduction via Stepwise Refinement 116
8.2 Reduction to Single-Step Theorems 116
8.3 Equivalences and Auxiliary Variables 120
8.4 Examples 122
8.4.1 An ESI Cache Coherence Protocol 122
8.4.2 An Implementation of the Bakery Algorithm 125
8.4.3 A Concurrent Deque Implementation 130
8.5 Summary 135
8.6 Bibliographic Notes 135
9 Pipelined Machines 137
9.1 Simulation Correspondence, Pipelines, and Flushing Proofs 137
9.2 Reducing Flushing Proofs to Refinements 140
9.3 A New Proof Rule 142
9.4 Example 143
9.5 Advanced Features 147
9.5.1 Stalls 147
9.5.2 Interrupts 147
9.5.3 Out-of-Order Execution 148
9.5.4 Out-of-Order and Multiple Instruction Completion 148
9.6 Summary 149
9.7 Bibliographic Notes 150
Part IV Invariant Proving 152
10 Invariant Proving 153
10.1 Predicate Abstractions 155
10.2 Discussion 157
10.3 An Illustrative Example 158
10.4 Summary 160
10.5 Bibliographic Notes 161
11 Predicate Abstraction via Rewriting 162
11.1 Features and Optimizations 166
11.1.1 User-Guided Abstraction 167
11.1.2 Assume Guarantee Reasoning 167
11.2 Reachability Analysis 168
11.3 Examples 169
11.3.1 Proving the ESI 169
11.3.2 German Protocol 171
11.4 Summary and Comparisons 172
11.5 Bibliographic Notes 174
Part V Formal Integration of Decision Procedures 175
12 Integrating Deductive and Algorithmic Reasoning 176
13 A Compositional Model Checking Procedure 179
13.1 Formalizing a Compositional Model Checking Procedure 180
13.1.1 Finite State Systems 180
13.1.2 Temporal Logic formulas 181
13.1.3 Compositional Procedure 181
13.2 Modeling LTL Semantics 183
13.3 Verification 187
13.4 A Deficiency of the Integration and Logical Issues 190
13.5 A Possible Remedy: Integration with HOL4 192
13.6 Summary and Discussion 193
13.7 Bibliographic Notes 194
14 Connecting External Deduction Tools with ACL2 195
14.1 Verified External Tools 196
14.1.1 Applications of Verified External Tools 200
14.1.1.1 Adding a Hypothesis 200
14.1.1.2 Equality Reasoning 201
14.1.1.3 Sorting Bit Vector Addition 202
14.2 Basic Unverified External Tools 203
14.2.1 Applications of Unverified External Tools 204
14.3 Unverified External Tools for Implicit Theories 205
14.4 Remarks on Implementation 209
14.4.1 Basic Design Decisions 209
14.4.2 Miscellaneous Engineering Considerations 211
14.5 Summary 214
14.6 Bibliographic Notes 215
Part VI Conclusion 217
15 Summary and Conclusion 218
References 221
Index 235