Hardware and Software: Verification and Testing
5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009, Revised Selected Papers
Published on 10. February 2011
X, 169 pages
978-3-642-19237-1 (ISBN)
Description
This book constitutes the thoroughly refereed post proceedings of the 5th International Haifa Verification Conference, HVC 2009, held in Haifa, Israel in October 2009. The 11 revised full papers presented together with four abstracts of invited lectures were carefully reviewed and selected from 23 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).
More details
Other editions
Additional editions
Kedar Namjoshi | Andreas Zeller | Avi Ziv
Hardware and Software: Verification and Testing
5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009, Revised Selected Papers
Book
02/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- I Keynote and Invited Talks
- Can We Verify an Elephant?
- Pain, Possibilities, and Prescriptions Industry Trends in Advanced Functional Verification
- The SBSE Approach to Automated Optimization of Verification and Testing
- DART: Directed Automated Random Testing
- II Research Papers
- Reduction of Interrupt Handler Executions for Model Checking Embedded Software
- Introduction
- [mc]square
- Reduction of Interrupt Handler Executions
- General Idea
- Static Analysis
- An Example
- Formal Model and Correctness Proof
- The Formal Model
- Correctness of the Abstraction
- Case Study
- Related Work
- Conclusion and Future Work
- References
- Diagnosability of Pushdown Systems
- Introduction
- Diagnosability and Bounded Latency
- Pushdown Systems
- Diagnosability and Bounded Latency of pd Systems
- Extension to Higher-Order Pushdown Systems
- References
- Functional Test Generation with Distribution Constraints
- Introduction
- Background
- Distribution Constraints
- Problem Definition
- Algorithms for CP with Distribution Constraints
- CSP Formulation for SCSPD and MCSPD
- Feasible Property Subsets
- CP Search Based Algorithm with Parallelization Scheme for SCSPD
- Probabilistic LP Based Algorithm for SCSPD
- Probabilistic LP Based Algorithm for MCSPD
- Experimental Results
- Conclusion
- References
- An Explanation-Based Constraint Debugger
- Introduction
- GenDebugger - Explanation-Based Debugging
- GenDebugger and Explanations
- Full Explanations
- Debugging Various Constraint-Related Problems
- Understanding a Constraint Conflict
- Understanding Value Assignments
- Understanding Distribution
- Understanding Performance
- GenDebugger Experience
- References
- Evaluating Workloads Using Multi-comparative Functional Coverage
- Introduction
- Algorithms and Tooling
- Fundamentals and Definitions
- Comparing Raw Data from Multiple Data Sources
- Single and Grouping Comparison
- Naming Algorithm
- Initial Experiences
- Conclusions
- References
- Reasoning about Finite-State Switched Systems
- Introduction
- Transducers and Switched Systems
- The Input-Output Language of a Switched System
- Compositional Model Checking
- Synthesis of a Switching Rule
- Undecidable Problems
- Synthesis of a Switching Rule
- Language Characterization
- References
- Dataflow Analysis for Properties of Aspect Systems
- Introduction
- Related Work
- Categories and Their Implications
- Advice Categories
- Provided Services of Introduced Methods
- Maintained Properties of Advice Categories
- Strongly Invasive Advice
- Spectative Advice
- Regulative Advice
- Public-Call-Correcting Advice
- Control-Safe Advice
- Relations
- Detection of the Defined Categories
- Summaries
- Exact-Proceed Analysis
- Slicing
- Experience
- Conclusions
- References
- Bisimulation Minimisations for Boolean Equation Systems
- Introduction
- Preliminaries
- Equivalences
- Strong Bisimilarity
- Idempotence-Identifying Bisimulation
- Decidability
- Experiments
- Process Equivalence Experiments
- Model Checking Experiments
- Discussion
- Conclusions
- References
- Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming
- Introduction
- Preliminaries
- The Leader Election Problem
- Model Checking Based Genetic Programming
- Generating Parametric Programs
- State Space Reduction
- Convergence for Parametric Problems
- Experimental Results
- Conclusions
- References
- Stacking-Based Context-Sensitive Points-to Analysis for Java
- Introduction
- Weighted Pushdown Model Checking
- Semantics and Abstraction
- Java Semantics on the Heap and Call Stack
- Abstraction
- Detecting Points-to Information by Model Checking
- Acceleration by Lightening Iterative Cycles
- A Traditional Iterative Procedure Scheme
- A Two-Staged Iterative Procedure Scheme
- Adding Summary Transition Rules in LE
- Empirical Studies
- Related Work
- Conclusions
- References
- An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
- Introduction
- Preliminaries
- A Graph-Based Decision Procedure
- Extracting Interpolants from Contradictory Cycles
- Application and Evaluation
- Related Work
- Conclusion and Future Work
- References
- Author Index
