HVC 2009
Haifa Verification Conference 2009
October 19-22, 2009
Organized by IBM R&D Labs in Israel

| Program |
|---|
| Conference program PDF version for printing (56 KB) |
| Tutorials program PDF version for printing (481 KB) |
| October 19, 2009 - Tutorials | |
|---|---|
| 09:30 | Registration |
| 10:00 | Morning Tutorial - Post Silicon 101 |
| 13:00 | Lunch |
| 14:30 | Afternoon Tutorial I - Satisfiability Modulo Theories (SMT) |
| 16:00 | Break |
| 16:30 | Afternoon Tutorial II - Constraints Satisfaction Problems (CSP) for Verification |
| October 20, 2009 | |
|---|---|
| 08:30 | Registration |
| 09:00 | Opening Remarks |
| 09:30 | Keynote Talk: |
| The SBSE Approach to Automated Optimization of Verification and Testing Mark Harman, CREST centre at King's College London |
|
| 10:30 | Coffee Break |
| 11:00 | Invited Session - The History of Verification Session Chair: Karen Yorav, IBM |
| Speakers: Andreas Zeller, University of Saarland Janick Bergeron, Synopsys Orna Kupferman, Hebrew University |
|
| 13:00 | Lunch |
| 14:30 | Paper Session I Session Chair: Orna Kupferman, Hebrew University |
| Dataflow Analysis for Properties of Aspect Systems Yevgenia Alperin and Shmuel Katz |
|
| Stacking-based Context-Sensitive Points-to Analysis for Java Xin Li and Mizuhito Ogawa |
|
| 15:30 | Coffee Break |
| 16:00 | Panel - The Future of Verification Moderator: Avi Ziv, IBM |
| Panelists: Harry Foster, Mentor Graphics Mark Harman, , CREST centre at King's College London Yoav Hollander, Cadence Ofer Strichman, Technion |
|
| 17:30 | Cocktail Party |
| October 21, 2009 | |
|---|---|
| 09:00 | Registration |
| 09:30 | Paper Session II Session Chair: Doron Peled, Bar Ilan University |
| Reduction of Interrupt Handler Executions for Model Checking Embedded Software Bastian Schlich, Thomas Noll, Joerg Brauer, and Lucas Brutschy |
|
| Functional Test Generation with Distribution Constraints Anna Moss and Boris Gutkovich |
|
| 10:30 | Coffee Break |
| 11:00 | Invited Session - Influential EU Software Testing Projects Session Chair: Shmuel Ur, IBM |
| Speakers: Tanja Vos, Technical University of Valencia Onn Shehory, IBM | |
| 12:00 | Paper Session III Session Chair: Gil Shurek, IBM |
| An Explanation-Based Constraint Debugger Aaron Rich, Giora Alexandron, and Reuven Naveh |
|
| Evaluating Workloads Using Multi-Comparative Functional Coverage Yoram Adler, Dale Blue, and Shmuel Ur |
|
| 13:00 | Lunch |
| 14:00 | Invited Talk: |
| Pain, Possibilities, and Prescriptions Industry Trends in Advanced Functional Verification Harry Foster, Mentor Graphics |
|
| 15:00 | Nazareth Excursion |
| October 22, 2009 | |
|---|---|
| 09:00 | Registration |
| 09:30 | Paper Session IV Session Chair: Orna Grumberg, Technion |
| Synthesizing Solutions to the Leader Election Problem using Model Checking and Genetic Programming Gal Katz and Doron Peled |
|
| Reasoning about Finite-State Switched Systems Dana Fisman and Orna Kupferman |
|
| 10:30 | Coffee Break |
| 11:00 | Keynote Talk: |
|
Can We Verify an Elephant? David Harel, Weizmann Institute of Science |
|
| 12:00 | HVC Award Presentation |
| DART: Directed Automated Random Testing Koushik Sen, UC Berkeley |
|
| 13:00 | Lunch |
| 14:30 | Paper Session V Session Chair: Hana Chockler, IBM |
| Bisimulation Minimisations for Boolean Equation Systems Jeroen Keiren and Tim Willemse |
|
| Diagnosability of Pushdown Systems Christophe Morvan and Sophie Pinchinat |
|
| An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions Daniel Kroening and Georg Weissenbacher / |
|
| 16:00 | Closing Remarks |

