Hardware and Software: Verification and Testing
6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers
Erschienen am 9. März 2011
X, 197 Seiten
978-3-642-19583-9 (ISBN)
Beschreibung
This book constitutes the thoroughly refereed post-conference proceedings of the 6th International Haifa Verification Conference, HVC 2010, held in Haifa, Israel in October 2010.
The 10 revised full papers presented together with 7 invited papers were carefully reviewed and selected from 30 submissions. The papers address all current issues, challenges and future directions of verification for hardware, software, and hybrid systems and have a research focus on hybrid methods and the migration of methods and ideas between hardware and software, static and dynamic analysis, pre- and post-silicon.
Weitere Details
Weitere Ausgaben
Andere Ausgaben
Sharon Barner | Ian Harris | Daniel Kroening
Hardware and Software: Verification and Testing
6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers
Buch
03/2011
Springer
53,49 €
Versand in 7-9 Tagen
Inhalt
- Title
- Preface
- Organization
- Table of Contents
- Understanding Transactional Memory
- References
- The SMT-LIB Initiative and the Rise of SMT
- Testing Concurrent Software
- Introduction
- Reflections on Spartan Programming and the No-Debugger Principle
- Spartan Programming
- No-Debugger Principle: DALUT SOREFET
- An Introduction to Test Specification in FQL
- Introduction
- The Language Design Challenge
- Quoted Regular Expressions
- The FQL Language Concept
- Path Patterns: Regular Expressions
- Coverage Specifications: Quoted Regular Expressions
- Target Graphs and Filter Functions
- Target Alphabet: CFA Edges, Nodes, Paths
- Full FQL Specifications
- Example Specifications
- Tool Support
- Related Work
- Conclusion
- References
- Verification Failures: What to Do When Things Go Wrong
- Special Session on Debugging
- Introduction
- Challenges in Debugging
- BackSpace: Formal Methods for Post-Silicon Debugging
- Debugging of Parallel and Distributed Programs
- References
- Debugging Unrealizable Specifications with Model-Based Diagnosis
- Introduction
- Preliminaries
- Model-Based Diagnosis
- Games and the -Calculus
- Specifications for Reactive Systems
- Minimization Algorithms
- Model-Based Diagnosis for Unrealizability
- Property Specifications
- Assumption/Guarantee Specifications
- Diagnosing Variables
- Implementation
- Efficient Implementation for GR(1) Specifications
- Experimental Results
- Example
- Performance Evaluation
- Conclusion
- References
- Parallelizing a Symbolic Compositional Model-Checking Algorithm
- Introduction
- Background
- Parallelizing the Split-Invariance Calculation
- Parallelizing the Least Fixpoint Evaluation
- Bdd Implementation Issues
- Implementation Decisions
- Experiments and Results
- The Examples
- Comments and Observations
- Related Work and Conclusions
- References
- Reaching Coverage Closure in Post-silicon Validation
- Introduction
- Post-silicon Validation
- Stimuli Generation
- Checking
- Coverage
- Reaching Coverage Closure in Pre-silicon
- Reaching Coverage Closure in Post-silicon
- Harvesting Algorithm for Post-silicon
- Case Study - POWER7 Core
- Conclusions
- References
- Variants of LTL Query Checking
- Introduction
- Achieving Objective O2
- The Construction
- An Algorithm for a Single Placeholder
- Reductions
- Complexity
- Multiple Placeholders
- Objectives O1 and O3
- Achieving Objective O1
- Achieving Objective O3
- Conclusions and Future Work
- References
- SAT-Solving Based on Boundary Point Elimination
- Introduction
- Basic Definitions
- Boundary Points and Resolution
- Boundary Points and Their Properties
- Elimination of Boundary Points by Adding Resolvents
- BPE-SAT
- Justification of BPE-SAT
- High-Level View of BPE-SAT
- The BPE Procedure
- Description of elim_bnd_pnts Procedure
- Quantification by Boundary Point Elimination
- CDCL SAT-Solvers in Terms of BPE
- Applying BPE-SAT to Solving Narrow Formulas
- Some Background
- Experimental Results
- Conclusions
- References
- Feedback-Based Coverage Directed Test Generation: An Industrial Evaluation
- Introduction
- Background
- Coverage Directed Test Generation
- Evolutionary Algorithms
- MicroGP
- FirePath
- FireDrill
- Experimental Setup
- Overview
- Test Program Representation
- Comparing Performance
- Experimental Evaluation
- Experimental Configuration
- Results - Single Best
- Results - Cumulative
- Results - Coverage Progression
- Discussion
- Conclusions
- References
- vlogsl: A Strategy Language for Simulation-Based Verification of Hardware
- Introduction
- vlogsl
- Four Strategy Examples
- Case Study: I2C-Bus Master Controller
- Related Work
- Conclusion
- References
- Advances in Simultaneous Multithreading Testcase Generation Methods
- Introduction
- SMT Verification History at IBM
- The MP-Based SMT Generation Technique
- The Thread Irritation Technique
- SMT Verification in POWER7
- POWER7 Verification Results
- Thread Irritation on Post-silicon
- Discussion
- References
- Revisiting Synthesis of GR(1) Specifications
- Introduction
- Preliminaries
- Temporal Logic and Tree-Models
- Realizability of Temporal Specifications
- The Syntactic Reduction Is Incomplete
- Synthesis of Reactive(1) Designs
- Incompleteness
- Well-Separated Environments
- General Specifications
- Conclusions
- References
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Introduction
- Preliminaries and Previous Work
- The RecyclePivots Approach
- Local Proof Transformation Rules
- Reduction by Proof Manipulation
- Two New Reduction Rules
- The Transformation Algorithm
- Duplications and Heuristics
- Comparison with RecyclePivots and Combination
- Experiments
- Conclusion
- References
- Author Index
