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

Haifa Verification Conference 2008

IBM Haifa Labs


October 27-30, 2008
Organized by IBM Haifa Research Lab

  • Program PDF version for printing (667 KB)
  • Tutorial

    October 28, 2008

    8:30 Registration

    9:00 Opening Remarks,
    Moshe Levinger, IBM Haifa Research Lab

    Session I
    Session chair: Ken McMillan

    Keynote Talk

    9:30 Hazards of Verification,
    Daniel Jackson, MIT

    10:30 Efficient Decision Procedure for Bounded Integer Non-linear Operations Using SMT(LIA),
    Malay Ganai (Presentation)

    11:00 Coffee Break

    Session II
    Session chair: Malay Ganai

    11:30 Synthesizing Test Models from Test Cases,
    Antti Jääskeläinen, Antti Kervinen, Mika Katara, Antti Valmari and Heikki Virtanen (Presentation)

    12:00 A Meta Heuristic for Effectively Detecting Concurrency Errors,
    Neha Rungta and Eric Mercer (Presentation)

    12:30 Evaluating Workloads Using Comparative Functional Coverage,
    Yoram Adler, Dale Blue, Thomas Conti, Richard Prewitt and Shmuel Ur

    13:00 Iterative Delta Debugging,
    Cyrille Valentin Artho (Presentation)

    13:30 Lunch

    Session III
    Session chair: Moshe Vardi

    15:30 Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta- Sigma Modulator,
    Edmund Clarke, Alexandre Donzé, and Axel Legay (Presentation)

    16:00 Coffee Break

    Session IV
    Session chair: Daniel Jackson

    16:30 Tool Presentation: SeeCode - A Code Review Plug-in for Eclipse,
    Moran Shochat, Orna Raz and Eitan Farchi (Presentation)

    16:45 Tool Presentation: Progress in Automated Software Defect Prediction,
    Elaine Weyuker and Thomas Ostrand (Presentation)

    17:00 Significant Diagnostic Counterexamples in Probabilistic Model Checking,
    Miguel E. Andrés, Pedro R. D'Argenio and Peter van Rossum (Presentation)

    17:30 A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata,
    Kerstin Bauer, Raffaella Gentilini and Klaus Schneider (Presentation)

    18:00 Cocktail Party

    October 29, 2008

    Session I
    Session chair: Alan Hu

    9:15 Best Paper and HVC Award Presentations

    9:30 HVC Award Winner: Proofs, Interpolants, and Relevance Heuristics,
    Ken McMillan

    10:15 Invited Talk: Is Verification Getting Too Complex?,
    Yoav Hollander, Cadence (Presentation)

    11:00 Coffee Break

    Session II
    Session chair: Orna Grumberg

    11:30 Panel: Coverage Metrics Across the Verification Domain

    13:15 Lunch

    Session III
    Session chair: Carl Pixley

    14:30 Invited talk: Can Mutation Analysis Help Fix Our Broken Coverage Metrics?,
    Brian Bailey (Presentation)

    15:15 Automatic Boosting of Cross-Product Coverage Using Bayesian Networks,
    Dorit Baras, Avi Ziv, and Laurent Fournier (Presentation)

    15:45 Coffee Break

    16:00 Caesarea Excursion and Dinner

    October 30, 2008

    Session I
    Session chair: Doron Peled

    Keynote Talk

    9:15 Automata-Theoretic Model Checking Revisited,
    Moshe Vardi, Rice University (Presentation)

    10:15 A Framework for Inherent Vacuity,
    Orna Kupferman, Dana Fisman, Moshe Vardi and Sarai Sheinvald (Presentation)

    10:45 Coffee Break

    Session II: Post-Silicon Verification (invited session)
    Session chairs: Ziyad Hanna and Warren Hunt

    11:15 Contemporary Post-Silicon Verification Mechanisms,
    Warren Hunt, UT Austin

    11:45 A Mechanized Framework for Applying Formal Analysis in Post-silicon Verification,
    Warren Hunt, UT Austin

    12:15 Application of Formal Technology in Post Silicon Verification and Debugging,
    Jamil Mazzawi, Jasper (Presentation)

    12:45 Multi-threading Post Silicon Exerciser - ThreadMill,
    Amir Nahir, IBM HRL (Presentation)

    13:15 Lunch

    Session III
    Session chair: Jason Baumgartner

    14:30 Invited talk: Practical Considerations Concerning HL-to -RT Equivalence Checking,
    Carl Pixley, Synopsys (Presentation)

    15:15 Tool Presentation: User-Friendly Model Checking: Automatically Configuring Algorithms with RuleBase/PE,
    Ziv Nevo (Presentation)

    15:30 Tool Presentation: D-TSR: Parallelizing SMT-based BMC Using Tunnels over Distributed Framework,
    Malay Ganai and Weihong Li

    15:45 Coffee Break

    Session IV
    Session chair: Karen Yorav

    16:15 Linear-time Reductions of Resolution Proofs,
    Omer Barilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham and Ofer Strichman (Presentation)

    16:45 Structural Contradictions,
    Cindy Eisner and Dana Fisman (Presentation)

    17:15 Closing Remarks


        About IBMPrivacyContact
    Caesarea Rothschild Institute (CRI) IBM Research