Skip to main content
    Israel [change]    Terms of use
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

Haifa Verification Conference 2007

IBM Haifa Labs


October 23 - 25, 2007
Organized by IBM Haifa Research Lab

  • List of accepted papers
  • Program PDF version for printing (211 KB)
  • The tutorial program

    Tuesday, October 23

    09:00 Registration

    09:15 Opening Remarks,
    Oded Cohn, IBM Haifa Research Lab

    Keynote Talk

    09:45 Microprocessor Verification Challenges,
    Bob Bentley, Intel Corporation

    10:45 Break

    Session I: Hardware Verification

    11:15 Invited talk: Out of Steam? - From "Hardware Verification Crisis" to "Crisis of Verification",
    Wolfgang Roesner, IBM Austin
    (Presentation - 4,048 KB)

    12:00 On the Characterization of Until as a Fixed Point Under Clocked Semantics,
    Dana Fisman
    (Presentation - 5,768 KB)

    12:30 Reactivity in SystemC Transaction-Level Models,
    Frederic Doucet, R.K. Shyamasundar, Ingolf H. Krueger, Saurabh Joshi, and Rajesh K. Gupta
    (Presentation - 362 KB)

    13:00 Lunch

    Session II: Model Checking

    14:15 Verifying Parameterised Hardware Designs via Counter Automata,
    Ales Smrčka and Tomas Vojnar
    (Presentation - 323 KB)

    14:45 How Fast and Fat is your Probabilistic Model Checker?,
    David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Mariëlle Stoelinga, and Ivan Zapreev
    (Presentation - 3,691 KB)

    15:15 Break

    Session III: Dynamic Hardware Verification

    15:45 Constraint Patterns and Search Procedures for CP-Based Random Test Generation,
    Anna Moss

    16:15 Using Virtual Coverage to Hit Hard-To-Reach Events,
    Laurent Fournier and Avi Ziv
    (Presentation - 435 KB)

    16:45 Cocktail party

    Wednesday, October 24

    Session I: HVC Award

    09:15 Best Paper and HVC Award Presentations

    09:30 HVC Award Winner: Symbolic Execution and Model Checking for Testing,
    Corina Pasareanu, NASA Ames Research Center
    (Presentation - 2,967 KB)

    10:30 Speed Networking Session

    Session II: Merging Formal and Testing

    11:15 Invited talk: Simulation vs. Formal: Absorb What is Useful; Reject What is Useless
    The Bruce Lee Approach to Verification
    Alan Hu, Univ. of British Columbia
    (Presentation - 581 KB)

    12:00 Test Case Generation for Ultimately Periodic Paths,
    Saddek Bensalem, Doron Peled, Hongyang Qu, Stavros Tripakis, and Lenore Zuck
    (Presentation - 1,369 KB)

    12:30 Dynamic Testing via Automata Learning,
    Harald Raffelt, Bernhard Steffen, and Tiziana Margaria

    13:00 Lunch

    Session III: Large Systems Verification

    14:15 Invited talk: Scaling Commercial Verification to Larger Systems,
    Robert Kurshan, Cadence
    (Presentation - 2,702 KB)

    15:30 Excursion

    Thursday, October 25

    Keynote Talk

    09:30 From Hardware Verification to Software Verification: Re-use and Re-learn,
    Aarti Gupta, NEC Labs America
    (Presentation - 861 KB)

    10:30 Break

    Session I: Formal Verification for Software

    11:00 On the Architecture of System Verification Environments,
    Mark A. Hillebrand and Wolfgang J. Paul
    (Presentation - 870 KB)

    11:30 Exploiting Shared Structure in Software Verification Conditions,
    Domagoj Babic and Alan J. Hu
    (Presentation - 126 KB)

    12:00 Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code,
    Thomas Noll and Bastian Schlich
    (Presentation - 442 KB)

    12:30 A Complete Bounded Model Checking Algorithm for Pushdown Systems,
    Gerard Basler, Daniel Kroening, and Georg Weissenbacher
    (Presentation - 1,102 KB)

    13:00 Lunch

    Session II: Software Bugs

    14:15 Invited talk: Where Do Bugs Come From?,
    Andreas Zeller, Saarland University
    (Presentation - 20,496 KB)

    15:15 Locating Regression Bugs,
    Dor Nir, Shmuel Tyszberowicz, and Amiram Yehudai
    (Presentation - 1,491 KB)

    15:45 Break

    Session III: Software Testing

    16:15 The Advantages of Post-link Code Coverage,
    Orna Raz, Moshe Klausner, Nitzan Peleg, Gad Haber, Eitan Farchi, Shachar Fienblit, Yakov Filiarsky, Shay Gammer, and Sergey Novikov
    (Presentation - 1,093 KB)

    16:45 GenUTest: A Unit Test and Mock Aspect Generation Tool,
    Benny Pasternak, Shmuel Tyszberowicz, and Amiram Yehudai
    (Presentation - 245 KB)

    17:15 Closing Remarks


        About IBMPrivacyContact
    Caesarea Rothschild Institute (CRI) IBM Research