Skip to main content

IBM R&D Labs in Israel News

Can We Verify an Elephant?

HVC 2009 gathered over 100 experts to determine future trends in software and hardware verification

Can we verify an elephant? According to David Harel, keynote speaker at the recent 2009 Haifa Verification Conference (HVC 2009), the answer seems to be yes. Harel showed how techniques from computer science can be applied to create comprehensive and realistic models of biological systems and help explain how they work. This and other talks at the fifth annual Haifa Verification Conference (HVC 2009) filled the auditorium at the IBM Research Lab in Haifa, Israel. The event drew a dynamic crowd of experts from industry and academia who attended to discuss how they can help each other and learn about new trends that combine both software and hardware verification.

‘There’s a solid core of participants who make it their business to attend HVC each year,” noted one enthusiastic participant. “We came to hear about new breakthrough research, get an infusion of knowledge from the keynote speakers, and connect up with new or old colleagues who are working on similar challenges.”

Another scientist who came all the way to Israel for HVC 2009 summed up the event. “I think everyone came away with something, whether new information or meeting new people. It was well organized and a lot of fun.”

Knowledge sharing and hybrid approaches


  HVC General Chair Avi Ziv (left) and
  HVC Keynote Mark Harman
“HVC is unique in bringing together verification experts in an atmosphere that blends the mostly disparate worlds of software testing and hardware verification—both dynamic and formal," explained Avi Ziv, IBM researcher for simulation-based verification and general chair of this year’s conference. “Not only does the conference bring together people from these two worlds, it also promotes knowledge sharing and new hybrid approaches to overcoming some of the more challenging hurdles in this domain,” continued Ziv. This year’s organizers set out to help people learn from each other and take these ideas home to develop new approaches to their work.

This year’s program covered a wide range of verification topics that focused on ‘where we’ve come from’ and ‘where we’re going’. As anticipated, the keynotes and the invited speakers were especially thought provoking. David Harel discussed the application of software engineering techniques to modeling biological systems in his talk “Can We Verify an Elephant.” Harry Foster provided an analysis of today’s trends and introduced new models for improving verification methods within an organization, in his talk on “Pain, Possibilities, and Prescriptions - Industry Trends in Advanced Functional Verification.” Mark Harman gave an overview of Search-Based Software Engineering (SBSE) applications to testing, verification and debugging—introducing many of the conference goers to this new topic for the first time.

Finding new answers to emerging challenges


During a break at HVC 2009
 
Another highlight was the conference panel on The Future of Verification, which focused on the directions from which new problems will arise and how different domains can help solve these problems.

Panel participants agreed on the foundations of new challenges facing the future of verification. With hardware development becoming more abstract and the increased use of prepared components, design times are getting shorter all the time. Moreover, new multi-core designs and multi-threaded programs are making it increasingly difficult to check for bugs. Now that designs are more complex and harder to verify, Ziv sees a major challenge in finding new ways to provide verification of the same quality in less time.

“Many solutions to verification challenges will be seeded by a union of hardware and software techniques,” feels Ziv. “Hopefully, merging knowledge in these domains will bring us new answers to the challenges ahead.”

 

Verification at HRL

IBM Research - Haifa has long been considered an IBM center of excellence for verification and testing research. Researchers there have developed several leading verification tools and methods in the following departments: