(Formal Methods in Computer Aided Design)

Hyatt Rickey's, Palo Alto, CA, Nov 3-6, 1998

Registration and Hotel/Transportation information



TUESDAY, Nov.3, 19:30-21:30: Registration and Reception, Hyatt Rickey's


7:00-8:45: Registration and Continental Breakfast

8:45-9.00: Welcome

9:00-10.00: Session 1: Invited talk, Dr. Kenneth McMillan. Title: Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification. Chair: Edmund Clarke

10:00-10:15: Coffee Break

10:15-11:15: Session 2: Processor Verification I. Chair: Mandayam Srivas.

10:15-10:45: Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution, Robert B. Jones, Jens U. Skakkebaek, and David Dill

10:45-11:15: Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking, Miroslav N. Velev and Randal E. Bryant

11:15-12:15: Session 3: Tools & Studies I. Chair: Albert Camilleri.

11:15-11:45: Solving Bit-Vector Equations, M.O. Moller and H. RueB

11:45-12:15: The formal design of 1M-gate ASICs, Asgeir Thor Eiriksson

12:15-1:30: Lunch served

1:30-2:30: Session 4: Boolean Methods I. Chair: Randal E. Bryant.

1:30-2:00: Design of Experiments for evaluation of BDD packages using controlled circuit mutations, Justin E. Harlow III and Franc Brglez

2:00-2:30: A tutorial on stalmarck's proof procedure for propositional logic , Mary Sheeran and Gunnar Stalmarck

2:30-3:30: Session 5: Tools & Studies II. Chair: Alan Hu.

2:30-3:00: Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods , Macha Nikolskaia, Antoine Rauzy, and David James Sherman

3:00-3:30: Bisimulation Minimization in an Automata-Theoretic Verification Framework, Kathi Fisler and Moshe Y. Vardi

3:30-3:45: Coffee Break

3:45-4:45: Session 6: Verification of Digital Abstraction. Chair: Ranga Vemuri.

3:45-4:15: Automatic verification of mixed-level logic circuits, Keith Hanna.

4:15-4:45: A timed automaton-based method for accurate circuit delay computation in the presence of cross-talk , S. Tasiran, S.P. Khatri, S. Yovine, R.K. Brayton, and A. Sangiovanni-Vincentelli

4:45-5:45: Session 7: Timing Issues and Verification. Chair: Tom Henzinger.

4:45-5:15: Maximum time separation of events in cyclic systems with linear and latest timing constraints , Fen Jin, Eduard Cerny, and Henrik Hulgaard

5:15-5:45: Using MTBDDs for composition and model checking of real-time systems Juergen Ruf and Thomas Kropf


7:00-9:00: Registration and Continental Breakfast

9:00-10.00: Session 8: Invited talk, Dr. Carl-Johan Seger. Title: Formal Methods in CAD from an Industrial Perspective. Chair: John Brzozowski.

10:00-10:15: Coffee Break

10:15-11:45: Session 9: Tools & Studies III. Chair: Steven Johnson.

10:15-10:45: A methodology for completely automatic verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool, Nazanin Manzouri and Ranga Vemuri

10:45-11:15: Combined Formal Post- and Presynthesis Verification in High Level Synthesis, Thomas Lock, Michael Mendler, and Matthias Mutz

11:15-11:45: Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem, Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan

11:45-1:00: Lunch served

1:00-2:00: Session 10: Special Talk: Prof. Randal E. Bryant and Bwolen Yang. Title: A Performance Study of BDD-based Model Checking. Chair: Jerry Burch.
Co-authors: David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev Ranjan, and Fabio Somenzi

2:00-2:15: Break.

2:15-3:15: Session 11: Model Checking I. Chair: Eduard Cerny.

2:15-2:45: Symbolic Model Checking Visualization, Gila Kamhi, Limor Fix, Ziv Binyamini

2:45-3:15: Input elimination and abstraction in model-checking, Sela Mador-Haim and Limor Fix

3:15-3:30: Coffee Break

3:30-4:30: Session 12: Symbolic Simulation Methods. Chair: Paul Loewenstein.

3:30-4:00: Symbolic Simulation of the JEM1 Microprocessor, David A. Greve

4:00-4:30: Symbolic Simulation: an ACL2 Approach, J. Strother Moore

4:30-5:15: Business Meeting

7:30-9:30: Session 13: Banquet. Speaker: Prof. Michael Flynn, Department of Electrical Engineering, Stanford. Title: Computer Arithmetic: Past, Present, and Future. Chair: David Dill


7:00-9:00: Registration and Continental Breakfast

9:00-10.00: Session 14: Invited talk, Prof. Amir Pnueli. Title: Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study Chair: J.Strother Moore
Co-author: T. Arons.

10:00-10:15: Coffee Break

10:15-11:15: Session 15: Processor Verification II. Chair: Steven German.

10:15-10:45: Combining symbolic model checking with uninterpreted functions for out of order processor verification, Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zhu

10:45-11:15: Formally Verifying Data and Control with Weak Reachability Invariants, Jeffrey Su, David Dill, and Jens U. Skakkebaek

11:15-12:15: Session 16: Modeling and Verification Methods I. Chair: Tom Shiple.

11:15-11:45: Generalized reversible Rules, Norris Ip

11:45-12:15: An Assume-Guarantee rule for checking simulation, T. A. Henzinger, S. Qadeer, S.K. Rajamani, and S. Tasiran

12:15-1:30: Lunch served

1:30-2:30: Session 17: Modeling and Verification Methods II. Chair: Thomas Kropf.

1:30-2:00: Three approaches to hardware verification: HOL, MDG, and VIS Compared, Sofiene Tahar, Paul Curzon, and Jianping Lu

2:00-2:30: An instruction set process calculus, Shiu-Kai Chin and Jang Dae Kim

2:30-3:30: Session 18: Model Checking II. Chair: Limor Fix.

2:30-3:00: Techniques for implicit state enumeration of EFSMs, James Kukula, Tom Shiple, and Adnan Aziz

3:00-3:30: Model checking on product structures, Klaus Schneider

3:30-3:45: Coffee Break

3:45-4:25: Session 19: An Overview of some FM tools. Chair: Michael J.C. Gordon.

3:45-3:55: BDDNOW : A Parallel BDD Package, Kim Milvang-Jensen and Alan J. Hu

3:55-4:05: Model-checking VHDL with CV, David Deharbe, Subash Shankar, and Edmund Clarke

4:05-4:15: Alexandria: A tool for hierarchical verification, Annette Bunker, Trent Larson, Michael Jones, Phillip Windley

4:15-4:25: PV: An Explicit Enumeration Model-checker, Ratan Nalumasu and Ganesh Gopalakrishnan

4:25-4:30: Closing Remarks & Best Paper Award

4:30-5:45: Tool Demos