Hardware and Software: Verification and Testing

1. Front Matter

   PDF

2. Keynote and Invited Talks

   1. Can We Verify an Elephant?

      • David Harel

      Pages 1-1

   2. Pain, Possibilities, and Prescriptions Industry Trends in Advanced Functional Verification

      • Harry Foster

      Pages 2-2

   3. The SBSE Approach to Automated Optimization of Verification and Testing

      • Mark Harman

      Pages 3-3

   4. DART: Directed Automated Random Testing

      • Koushik Sen

      Pages 4-4

3. Research Papers

   1. Reduction of Interrupt Handler Executions for Model Checking Embedded Software

      • Bastian Schlich, Thomas Noll, Jörg Brauer, Lucas Brutschy

      Pages 5-20

   2. Diagnosability of Pushdown Systems

      • Christophe Morvan, Sophie Pinchinat

      Pages 21-33

   3. Functional Test Generation with Distribution Constraints

      • Anna Moss, Boris Gutkovich

      Pages 34-51

   4. An Explanation-Based Constraint Debugger

      • Aaron Rich, Giora Alexandron, Reuven Naveh

      Pages 52-56

   5. Evaluating Workloads Using Multi-comparative Functional Coverage

      • Yoram Adler, Shmuel Ur, Dale Blue

      Pages 57-70

   6. Reasoning about Finite-State Switched Systems

      • Dana Fisman, Orna Kupferman

      Pages 71-86

   7. Dataflow Analysis for Properties of Aspect Systems

      • Yevgenia Alperin-Tsimerman, Shmuel Katz

      Pages 87-101

   8. Bisimulation Minimisations for Boolean Equation Systems

      • Jeroen J. A. Keiren, Tim A. C. Willemse

      Pages 102-116

   9. Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming

      • Gal Katz, Doron Peled

      Pages 117-132

   10. Stacking-Based Context-Sensitive Points-to Analysis for Java

       • Xin Li, Mizuhito Ogawa

       Pages 133-149

   11. An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions

       • Daniel Kroening, Georg Weissenbacher

       Pages 150-168

4. Back Matter

   PDF

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).

• automated random testing
• bisimulation minimization
• constraint debugging
• constraint-random verification
• dataflow analysis
• diagnosability
• distribution constraints
• formal reasoning
• functional test generation
• functional verification
• model checking
• multi-comparative functional coverage
• optimization of verification
• program analysis
• transitive relations

• Bell Laboratories, Alcatel-Lucent, Murray Hill, USA

  Kedar Namjoshi

• Saarland University, Saarbrücken, Germany

  Andreas Zeller

• IBM Research Laboratory, Haifa, Israel

  Avi Ziv

Policies and ethics