Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings

Description

This book constitutes the refereed proceedings of the 9th International Haifa Verification Conference, HVC 2013, held in Haifa, Israel in November 2013. The 24 revised full papers presented were carefully reviewed and selected from 49 submissions. The papers are organized in topical sections on SAT and SMT-based verification, software testing, supporting dynamic verification, specification and coverage, abstraction and model presentation. Front Matter....Pages - Backbones for Equality....Pages 1-14 PASS: String Solving with Parameterized Array and Interval Automaton....Pages 15-31 Increasing Confidence in Liveness Model Checking Results with Proofs....Pages 32-43 Speeding Up the Safety Verification of Programmable Logic Controller Code....Pages 44-60 Modeling Firmware as Service Functions and Its Application to Test Generation....Pages 61-77 Symbolic Model-Based Testing for Industrial Automation Software....Pages 78-94 Online Testing of LTL Properties for Java Code....Pages 95-111 Modbat: A Model-Based API Tester for Event-Driven Systems....Pages 112-128 Predictive Taint Analysis for Extended Testing of Parallel Executions....Pages 129-144 Continuous Integration for Web-Based Software Infrastructures: Lessons Learned on the webinos Project....Pages 145-150 SLAM: SLice And Merge - Effective Test Generation for Large Systems....Pages 151-165 Improving Post-silicon Validation Efficiency by Using Pre-generated Data....Pages 166-181 Development and Verification of Complex Hybrid Systems Using Synthesizable Monitors....Pages 182-198 Assertion Checking Using Dynamic Inference....Pages 199-213 Formal Specification of an Erase Block Management Layer for Flash Memory....Pages 214-229 Attention-Based Coverage Metrics....Pages 230-245 Synthesizing, Correcting and Improving Code, Using Model Checking-Based Genetic Programming....Pages 246-261 Domain Types: Abstract-Domain Selection Based on Variable Usage....Pages 262-278 Efficient Analysis of Reliability Architectures via Predicate Abstraction....Pages 279-294 Lazy Symbolic Execution through Abstraction and Sub-space Search....Pages 295-310 SPIN as a Linearizability Checker under Weak Memory Models....Pages 311-326 Arithmetic Bit-Level Verification Using Network Flow Model....Pages 327-343 Performance Evaluation of Process Partitioning Using Probabilistic Model Checking....Pages 344-358 Improving Representative Computation in ExpliSAT....Pages 359-364 Back Matter....Pages -