Verification, Model Checking, and Abstract Interpretation: 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010, Proceedings (Lecture ... Computer Science and General Issues)

This book constitutes the refereed proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010, held in Madrid, Spain, in January 2010. The 21 papers included in this volume were carefully reviewed and selected from 57 submissions. In addition 3 invited talks and 3 invited tutorials are presented. Topics covered by VMCAI include program verification, program certification, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. 3642113184......Page 1 Lecture Notes in Computer Science 5944......Page 2 Verification, Model Checking, and 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 This volume contains the proceedings of the 11th International Conference on Veri?cation, Model Checking, and Abstract Interpretation (VMCAI 2010), held in Madrid, Spain, January 17–19, 2010. VMCAI 2010 was the 11th in a series of meetings. Previous meetings were held in Port Je?erson (1997), Pisa (1998), Venice (2002), New York (2003), Venice(2004),Paris(2005),Charleston(2006),Nice(2007),SanFrancisco(2008), and Savannah (2009). VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, model checking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, model checking, debugging techniques, abstract interpretation, abstract domains, static analysis, type systems, deductive methods, and optimization. The Program Committee selected 21 papers out of 57 submissions based on anonymous reviews and discussions in an electronic Program Committee me- ing. The principal selection criteria were relevance and quality.