DIMACS Workshop on Computational and Complexity Issues in Automated Verification: Program

			PROGRAM

MONDAY, MARCH 25, 1996

  General tutorial/survey talks

08:50-09:00 Welcome - DIMACS Director or Associate Director

09:00-10:00  A. Pnueli
	     Temporal Logic 

10:00-11:00  E. Clarke, Carnegie Mellon University
	     Model Checking 

11:00-11:15  break

11:15-12:15  R. Bryant, Carnegie Mellon University
	     Overview of BDDs 

12:15-01:30 Lunch

  BDD session

01:30-02:00  S. Ponzio, MIT
	     Lower Bounds for BDDs 

02:00-02:30  F. Somenzi, University of Colorado, Boulder
	     Reordering Variables in Decision Diagrams 

02:30-03:00  R. Ranjan, University of California, Berkeley
	     Exploiting Memory Hierarchy for High Performance BDD Manipulation

03:00-03:30  break

  Partial Order verification

03:30-04:30  D. Peled, Lucent, Bell Labs 
	     Overview of Partial Order Verification 

04:30-05:00  P. Wolper 
	     Partial Order Methods or How Independence Defeats Complexity  


TUESDAY, MARCH 26, 1996

  Complexity and Expressiveness of Logical Theories

09:00-10:00  N. Immerman, University of Massachusetts
	     Finite Model Theory 
 
10:00-10:30  M. Vardi, Rice University
	     Automata on Infinite Strings 
 
10:30-11:00  break

11:00-11:30  A. Emerson, University of Texas, Austin 
	     Automata on Infinite Trees  

11:30-01:30 Lunch

  Program Checking

01:30-02:30  S. Kannan, University of Pennsylvania 
	     Overview of Checking, Self-Testing, and Self-Correcting 

02:30-02:45  Break

02:45-03:15  R. Rubinfeld, Cornell University and MIT
	     On the Robustness of Functional Equations 

03:15-03:45  F. Ergun, Cornell University and MIT
	     Testing Multivariate Linear Functions 

03:45-04:00  Break

04:00-04:30  R. Kumar, Cornell University and MIT 
	     Issues in Approximate Self-Testing 
 
04:30-05:00  H. Wasserman, University of California at Berkeley
	     Checking the Fourier Transform - A Historical Update 


WEDNESDAY, MARCH 27, 1996

    Synthesis 

09:00-10:00  N. Bjorner
	     Synthesis Survey 

10:00-10:30  A. Aziz, University of Texas, Austin
	     Optimization of Digital Circuits 

10:30-11:00  break

    Language Containment

11:00-12:00  R. Kurshan, Bell Labs
	     Future Directions 

12:00-12:30  O. Kupferman, Bell Labs
	     Experiences with Reduction Hierarchies 

12:30-02:00 Lunch

    Theory and Practice 

02:00-02:30  R. Alur, Bell Labs 
	     Principles for Hierarchical Reasoning 
 
02:30-03:00  S. German, IBM 
	     Verification of the SRT Division Algorithm 

03:00-03:30  A. Sistla
	     Homogeneous System Verification 

03:30-04:00  break


   Integrating Theorem Proving and Model Checking

04:00-04:30  N. Shankar, SRI 
	     The Integration of Model Checking with Theorem Proving in PVS
 
04:30-05:00  C. Seger, Intel
	     An Idiot Savant Theorem Prover for Hardware Verification 
   

THURSDAY, MARCH 28, 1996 

  Systems and Industrial Experience - I

09:00-10:00  K. McMillan, Cadence Berkeley Labs
	     Design by refinement using SMV 

10:00-10:30  D. Dill, Stanford University
	     Experience with Murphi 

10:30-11:00  break

11:00-12:00  G. de Palma, AT&T
	     Formalcheck/Cospan 

12:00-12:30  T. Shiple, University of California, Berkeley
	     VIS: A System for Verification and Synthesis 

12:30-02:00 Lunch

  Systems and Industrial Experience - II

02:00-03:00  G. Berry, INRIA, France
	     Esterel and Applications 

03:00-03:30  C. Pixley, Motorola
	     Formal and Informal Functional Verification at Motorola 

03:30-04:00  break

04:00-04:30  Xudong Zhao, CMU and Intel 
	     Word Level Model Checking for Arithmetic Circuits 

04:30-05:00  C. Eisner IBM 
	     Formal Verification in IBM: RuleBase, an 
	     Industrial-Strength Model-Checking Tool

05:00-05:30  H. Sipma, Stanford University
	     STeP 

Previous: Participation

Next: Registration

Workshop Index

DIMACS Homepage