Verification, Model Checking, and Abstract Interpretation: 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings

3642113184......Page 1
Lecture Notes in Computer Science 5944......Page 2
Verification,\rModel Checking,\rand Abstract Interpretation......Page 3
Preface......Page 5
Conference Organization......Page 7
Table of Contents......Page 9
Analysis of Systems with Stochastic Process Creation......Page 11
Verifying Concurrent Programs with Chalice......Page 12
Introduction......Page 13
The Architectural Challenge—and How to Cope with It......Page 15
A Timing Analysis Framework......Page 16
Cache Analysis......Page 18
Influence of the Cache Replacement Policy......Page 19
FIFO Cache Analysis......Page 22
Context Switch Costs......Page 25
Heap-Allocating Programs......Page 26
Symbolic Representation of Pipeline Domains......Page 27
Symbolic Domain and Analysis......Page 28
Optimizations and Performance......Page 29
References......Page 30
Abstract Interpretation-Based Protection......Page 33
Advances in Probabilistic Model Checking......Page 35
Building a Calculus of Data Structures......Page 36
Introduction......Page 37
Boolean Algebra with Presburger Arithmetic......Page 38
Multisets Algebra with Presburger Arithmetic......Page 39
NP Complexity of Multisets with Cardinality Constraints......Page 41
Algebraic Data Types with Abstraction Functions......Page 43
Examples of Applications......Page 44
The Decision Procedure......Page 46
A Completeness Criterion......Page 47
Combining Theories with Shared Set Operations......Page 48
Example: Proving a Verification Condition......Page 49
Combination by Reduction to BAPA......Page 51
BAPA Reductions......Page 52
References......Page 53
Introduction......Page 55
Nested Words......Page 57
A Simple Procedural Language......Page 58
Local Invariants and Summaries......Page 61
Temporal Verification......Page 63
References......Page 69
Introduction......Page 71
Preliminaries......Page 74
The Hierarchical Model-Checking Game......Page 78
Solving Hierarchical Parity Games......Page 79
An Abstraction-Refinement Paradigm......Page 84
References......Page 86
Introduction......Page 88
Definition of Convex Hybrid Automata......Page 89
Path and Path-Oriented Reachability......Page 90
Convex Encoding......Page 92
Problem Size......Page 94
Illustration......Page 95
Linear Flow Convex Hybrid Automata......Page 96
Monotonic Invariant Convex Hybrid Automata......Page 97
Case Studies......Page 98
Discussion on Potential Applications......Page 101
References......Page 103
Introduction......Page 105
Related Work......Page 107
Preliminaries......Page 108
Boolean Automata with Stores......Page 111
Lower Bounds for Boolean Automata......Page 112
Results......Page 115
Lower Bounds for Timed Automata with Store......Page 116
Upper Bounds for Timed Automata with Store......Page 117
Conclusions......Page 119
References......Page 120
Introduction......Page 122
Preliminaries......Page 124
Representation......Page 126
Constraint Comparison......Page 127
Projection......Page 128
Join......Page 130
Inclusion Test......Page 132
Widening......Page 133
Implementation......Page 134
Experiments......Page 135
References......Page 137
Introduction......Page 139
Finite State Model Checking......Page 140
Interpolant-Based Model Checking......Page 141
Resolution Refutations......Page 142
Interpolation Systems......Page 143
Interpolant Strength and Model Checking......Page 145
Labelling Functions and Interpolation......Page 146
Strength in Labelled Interpolation Systems......Page 148
Proof Transformations......Page 149
Proof Transformations and Interpolant Strength......Page 152
Conclusion......Page 153
References......Page 154
Introduction......Page 156
Bounded Event Tracing by Example......Page 157
Semantics of Unwindings......Page 160
Colored Contextual Unweighted Petri Nets......Page 161
Token Traces......Page 162
Encoding Token Traces......Page 163
Comparison to Related Work......Page 165
Unwindings of State Machine Models......Page 167
Experimental Evaluation......Page 169
Conclusions and Future Work......Page 170
References......Page 171
Introduction......Page 173
Related Work......Page 175
Motivating Example......Page 176
Programming Model......Page 177
Loop Synthesis......Page 180
Generation of Loop Invariants and Properties......Page 183
Implementation and Experiments......Page 185
Type Checking Matrices......Page 186
References......Page 188
Introduction......Page 190
The Target Language and Notation......Page 192
Framework Overview......Page 193
The CDNF Algorithm......Page 194
Learning Invariants......Page 196
Predicate Abstraction to Connect Algorithmic Learning and SMT Solvers......Page 197
Answering Queries from Algorithmic Learning......Page 198
Main Loop of Our Approach......Page 199
Experiments......Page 200
ide-ide-tape from Linux IDE Driver......Page 201
parser from VPR in SPEC2000 Benchmarks......Page 202
Discussion and Future Work......Page 203
Conclusions......Page 204
An Example of the CDNF Algorithm......Page 206
Introduction......Page 207
Congruent Closure......Page 209
Syntax of Flowchart Programs......Page 213
Semantic Equations......Page 214
Semantic Machinery: Encoding and Composition......Page 215
Semantic Equations......Page 216
Deriving Abstract Transitions......Page 217
Applying Abstract Transitions......Page 218
Transformation for Range Information......Page 219
Decomposing Guards......Page 220
Concluding Discussion......Page 221
References......Page 222
Introduction......Page 224
Preliminaries......Page 226
Fine-Grained Semantics and Analysis......Page 228
Coarse-Grained Semantics and Analysis......Page 231
Fine-Grained versus Coarse-Grained......Page 233
Application......Page 235
Related Work......Page 236
References......Page 238
Introduction......Page 241
Programs, Executions and Specifications......Page 243
Example......Page 244
Conformance Checker......Page 246
Instrumentation......Page 248
Bluetooth Driver......Page 249
Battery Driver......Page 251
Related Work......Page 253
Conclusion......Page 254
Embedding Thread-Modular Reasoning......Page 256
Introduction......Page 257
Example and Motivation......Page 258
Concrete Heap and Reference Set Relations......Page 260
Abstract Graphs......Page 261
Additional Instrumentation Predicates......Page 262
Operations......Page 264
Materialization......Page 265
Examples......Page 267
Experimental Evaluation......Page 269
Conclusion......Page 270
References......Page 271
Limitations of Control-Flow Analysis......Page 273
The Generalized Environment Problem......Page 275
State-Spaces......Page 276
Transition Rules......Page 277
Analogy: Singleton Abstraction to Binding Anodization......Page 279
Implementing Anodization Efficiently......Page 282
Analogy: Binding Invariants as Shape Predicates......Page 283
Solving the Generalized Environment Problem......Page 284
Related Work......Page 285
Future Work......Page 286
References......Page 287
Introduction......Page 289
Definitions and Notations......Page 290
An Example of Analysis......Page 291
Principles of the Analysis......Page 292
General Case......Page 294
A Solution Based on Linear Algebra......Page 296
Insertion Sort......Page 298
Combining the Analysis with Array Partitioning......Page 299
Other Examples......Page 300
Conclusion......Page 301
References......Page 302
Introduction......Page 305
Regular Expressions with Past......Page 307
Regular Linear Temporal Logic over Infinite Words......Page 310
LTL with Past......Page 312
From RLTL to Automata......Page 314
Complementing 2APW......Page 315
Translating from RLTL to 2APW......Page 316
Conclusion and Future Work......Page 319
References......Page 320
Introduction......Page 322
Related Work......Page 323
IRM Framework......Page 324
Verifier Overview......Page 325
Concrete Machine......Page 327
Abstract Machine......Page 329
An Abstract Interpretation Example......Page 331
Soundness......Page 332
Convergence......Page 333
Implementation......Page 334
Conclusion......Page 335
References......Page 336
Introduction......Page 338
A Considerate Specification of the Composite......Page 340
Considerate Reasoning......Page 342
Concerns-Descriptions......Page 343
Verification Technique......Page 347
Verification of the Composite Pattern......Page 349
Automation of Our Technique......Page 350
Conclusions, Related and Future Work......Page 352
References......Page 353
Introduction......Page 355
Underlying Separation Logic Domain......Page 356
RGSep......Page 357
Action Inference Algorithm......Page 359
Non-standard Join......Page 365
Evaluation......Page 366
Conclusion......Page 368
May-Subtraction Implementation......Page 370
Introduction......Page 372
Galois Connections, Best Transformers and Valuations......Page 374
Markov Decision Processes......Page 375
Lower- and Upper-Bound Abstraction......Page 376
Stochastic Games......Page 378
Best Transformers and Game-Based Abstraction......Page 379
Concurrent Probabilistic Programs......Page 381
Parallel Abstraction......Page 382
Parallel-Abstraction Games......Page 383
Refinement......Page 386
Experiments......Page 387
References......Page 388
Introduction......Page 390
Motivating Examples......Page 391
QFBAPA-Rel: A Logic of Sets, Cardinalities, Relations, and Unary Functions......Page 393
Decision Procedure for QFBAPA-Rel......Page 394
Complexity of QFBAPA-Rel......Page 397
Undecidable Extensions: Injective Binary Functions, Quantifiers......Page 398
NP-Complete Two-Sorted QFBAPA-Rel Fragment......Page 399
Logic of Multiset Images of Functions......Page 402
References......Page 404
Author Index......Page 406