This book constitutes the thoroughly refereed post-conference proceedings of the 4th International Haifa Verification Conference, HVC 2008, held in Haifa, Israel in October 2008.
The 12 revised full papers and 4 tool papers presented together with 6 invited lectures were carefully reviewed and selected from 49 initial submissions. The papers address all current issues, challenges and future directions of verification for hardware, software, and hybrid systems and present academic research in the verification of systems, generally divided into two paradigms - formal verification and dynamic verification (testing). Within each paradigm, different algorithms and techniques are used for hardware and software systems with a special focus on hybrid methods.
Author(s): Hana Chockler, Alan J. Hu
Edition: 1
Publisher: Springer
Year: 2009
Language: English
Pages: 215
front-matter.pdf......Page 1
Hazards of Verification......Page 11
Automata-Theoretic Model Checking Revisited......Page 12
Proofs, Interpolants, and Relevance Heuristics......Page 13
Is Verification Getting Too Complex?......Page 14
Can Mutation Analysis Help Fix Our Broken Coverage Metrics?......Page 15
Practical Considerations Concerning HL-to -RT Equivalence Checking......Page 16
Introduction......Page 17
Inherent Vacuity......Page 20
The Parameters of the Framework......Page 23
Working with the Different Parameters......Page 26
Discussion......Page 29
References......Page 31
Introduction......Page 33
Input Sequence......Page 35
Greedy Depth-First Search......Page 37
Guidance Strategy......Page 38
Study Design......Page 41
Error Discovery......Page 42
Effect of the Sequence Length......Page 44
Related Work......Page 45
References......Page 46
Introduction......Page 48
Preliminaries......Page 49
Abstractions of Hybrid Automata for Parallel over- and Underapproximated Reachability Analysis......Page 51
Discrete Bounded Bisimulation (DBB) Abstractions......Page 52
Modal Abstractions Based on May/Must Relations......Page 53
A Generic Semantics for $\mu$-Calculus on Abstractions of Hybrid Automata......Page 54
Semantics Completion for May/Must-Abstractions......Page 56
Semantics Completion for DBB Abstractions......Page 58
Abstraction Refinement and Monotonicity......Page 60
References......Page 61
Introduction......Page 63
Coverage Directed Generation Using Bayesian Networks......Page 65
A Bayesian Network for CDG......Page 66
The Coverage Booster......Page 67
Automatic Construction of CDG Engine......Page 68
Feature Selection......Page 69
Structure Learning......Page 70
Experiments......Page 72
References......Page 76
Introduction......Page 78
Our Approach: Overview......Page 79
Mixed Expressions and SMT......Page 80
Booleanization......Page 81
Bitwise Structural Decomposition (BSD)......Page 82
SHIFT......Page 83
Lazy Bounding and Refinement Procedure (LBR)......Page 84
Linearization Criteria......Page 86
Controlled Experimentation......Page 87
Experimentation with GCD/LCM Programs......Page 89
Experimentation with Benchmark C Programs......Page 90
Conclusion......Page 91
Introduction......Page 94
Workload Profiling with Empirical Data......Page 95
Functional Coverage Analysis......Page 98
Comparative Functional Coverage......Page 99
Comparative Functional Coverage Holes......Page 101
Experimental Results......Page 102
Conclusions......Page 107
References......Page 108
Introduction......Page 109
Intuition Behind IDD......Page 110
Delta Debugging......Page 112
Hierarchical Delta Debugging......Page 114
Compilation and Test Setup......Page 115
Test Evaluation Accuracy......Page 116
Implementation Architecture......Page 117
Experiments......Page 118
Uncrustify......Page 119
Java PathFinder......Page 120
Summary......Page 121
Future Work......Page 122
References......Page 123
Introduction......Page 124
Inference by Resolution......Page 127
Recycling Learned Unit Clauses......Page 128
Recycling Pivots......Page 131
Proofs......Page 133
The { c Recycle-Units} Algorithm......Page 134
Experimental Results and Conclusions......Page 136
References......Page 137
Introduction......Page 139
Markov Decision Processes......Page 142
Schedulers......Page 143
Linear Temporal Logic......Page 144
Counterexamples......Page 145
Representative Counterexamples, Partitions and Witnesses......Page 147
Rails and Torrents......Page 148
Significant Diagnostic Counterexamples......Page 152
Computing Most Indicative Torrent-Counterexamples......Page 154
Debugging Issues......Page 155
Final Discussion......Page 156
References......Page 157
Introduction......Page 159
Statistical Approach......Page 161
An Algorithmic Scheme......Page 162
Model......Page 163
Probabilistic Signal Linear Temporal Logic......Page 164
Verification Issues......Page 166
SSDES for a Third Order Modulator......Page 167
Experiments......Page 168
Future Work......Page 171
References......Page 172
Introduction......Page 174
Preliminaries......Page 176
Notation......Page 177
The Current Semantics of PSC......Page 178
Structural Contradictions......Page 179
The Solution......Page 180
Characteristics of the Truncated Semantics of psc......Page 184
Conclusion and Future Work......Page 187
References......Page 188
Introduction......Page 189
Model-Based GUI Testing of Mobile Software......Page 190
Synthesis of Test Models......Page 192
Action Definition......Page 193
Variable Definition and Integration......Page 194
State Label Definition and Assignment......Page 195
Merging of the Component Models......Page 196
Case Studies......Page 198
Discussion......Page 201
References......Page 202
Introduction......Page 204
TSR-Based BMC......Page 205
Tasks of the Master......Page 206
Tasks of a Client......Page 207
Experimentation......Page 208
References......Page 209
Research Overview......Page 210
Building a Tool......Page 211
Using the Tool......Page 212
References......Page 214
Introduction......Page 215
Code Review Perspective......Page 216
Distributed Review......Page 217
Deployment of SeeCode......Page 218
References......Page 219
Introduction......Page 220
Advisors......Page 221
Advice Selection......Page 222
Experimental Results......Page 223
References......Page 224
back-matter.pdf......Page 225
