IBM Research Lab in Haifa
IBM FV'2000 Summer Seminar - Agenda
  Day 1 – August 15 Day 2 – August 16 Day 3 – August 17
08:30-09:00 Registration    
09:00-09:15 Greetings - Michael Rodeh, Director of IBM HRL    
  Advanced State-Space Search Methods
(session chair: Y. Wolfsthal)
Advanced Model Reduction Methods
(session chair: O. Shtrichman)
Sat-Based Approaches

(session chair: T. Heyman)
09:15-10:00 Guided Search and Approximation Techniques for Symbolic Model Checking - F. Somenzi, Colorado University The Localization Reduction - B. Kurshan, Bell Labs A Journey into the World of SAT Solvers - A. Tacella, University of Genova
10:00-10:45 Prioritized Traversal: Efficient Reachability Analysis for Verification & Falsification - R. Fraer, Intel Improving Models Written by Novices - A. Hu, UBC Tuning SAT Checkers for Bounded Model Checking - O. Shtrichman, Weizmann Institute
10:45-11:00 Break Break Break
      State of the Practice
(session chair: Y. Wolfsthal)
11:00-11:45 Scalable Distributed Symbolic Model Checking - T. Heyman, IBM Haifa Research Lab Model Checking Systems with Many Subcomponents - A. Emerson, UT at Austin Formal Methods in the Development of Industrial Critical System - A. Cimatti, IRST
11:45-12:30 A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles - K. Ravi, Cadence A New Algorithm for Conjunction Scheduling in Image Computation - F. Somenzi, Colorado University Faithful Translations - S. Katz, Technion
12:30- Lunch Lunch Lunch
  Computation Models & Proof Strategies
(session chair: C. Eisner)
Industry Track I

(session chair: D. Geist)
State of the Practice (cont.)

(session chair: C. Eisner)
14:00-14:45 Sticks and Stones: Making the Most of a Single Unbounded Dimension - A. Pnueli, Weizmann. Institute Formal Verification in Galileo - G. Vardi, Galileo Technology A Methodology for Formal Design of Hardware Control with Applications to Cache Coherency Protocols - C. Eisner, IBM Haifa Research Lab
14:45-15:30 The Ultimate Specification Language - M. Vardi, Rice University Formal Methods in Processor Developments at AMD - D. Reed, AMD Notes on Technology Transfer - B. Kurshan, Bell Labs
15:30-16:15 Strategies for Combining Theorem Proving and Model Checking - K. McMillan, Cadence Verifying Configuration Register Logic using Formal Methods - E. Bokshtein, IBM Haifa Design Center Path Exploration Tool: a Tool for Interactive Software Testing - D. Peled, Bell Labs
16:15-17:00     Automatic Formal Verification of DSP Software - A. Hu, UBC
18:00 Cocktails    
19:00 Gala Dinner   Barbeque