Third International Conference on
Formal Methods in Computer-Aided Design

Advance Program
Wednesday, November 1, 2000
9:00 Combining Algebraic and Algorithmic Verification of Microarchitectures
Nancy Day, Mark Aagaard, Byron Cook
9:30 Applications of Hierarchical Verification in Model Checking
Robert Beers, Rajnish Ghughal, Mark Aagaard
10:00 Break
10:30 Modeling and Parameter Synthesis for an Air Traffic Management System
Adilson Luiz Bonifácio, Arnaldo Vieira Moura
11:00 Verifying transaction ordering properties in unbounded bus networks through combined
algorithmic/deductive methods

Michael Jones, Ganesh Gopalakrishnan
11:30 A Methodology for Large-Scale Hardware Verification
Mark Aagaard, Robert B Jones, Thomas F Melham, John W O'Leary, Carl-Johan H Seger
12:00 Lunch.
Welcome and State of the Conference Address
1:30 An n log n Symbolic Algorithm for Strongly Connected Component Analysis
Roderick Bloem, Harold N. Gabow, Fabio Somenzi
2:00 A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
Kavita Ravi, Roderick Bloem, Fabio Somenzi
2:30 Break
3:00 The Semantics of Verilog Using Transition System Combinators
Gordon J. Pace
3:30 A Theory of Consistency for Modular Synchronous Systems
Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel
4:00 Break
4:30 Visualizing System Factorizations with Behavior Tables
Alex Tsow, Steven D. Johnson
5:00 Scalable distributed on-the-fly symbolic model checking
Shoham Ben-David, Tamir Heyman, Orna Grumberg, Assaf Schuster
5:45 Planning Session for Next FMCAD.
Everyone Welcome
Thursday, November 2, 2000
9:00 Formal verification of floating point trigonometric functions
John Harrison
9:30 A Case Study in Formal Verification of Register-Transfer Logic with ACL2:
The Floating Point Adder of the AMD Athlon Processor

David Russinoff
10:00 Break
10:30 Correctness of Pipelined Machines
Panagiotis Manolios
11:00 Hardware Modeling Using Function Encapsulation
Jun Sawada, Warren A. Hunt, Jr.
11:30 A Methodology for the Formal Analysis of Asynchronous Micropipelines
Antonio Cerone, George Milne
12:00 Lunch
1:30 Automated Refinement Checking for Asynchronous Processes
Rajeev Alur, Radu Grosu, Bow-Yaw Wang
2:00 Model Reductions and a Case Study
Jin Hou, Eduard Cerny
2:30 Break
3:00 Border-Block Triangular Form and Conjunction Schedule in Image Computation
In-Ho Moon, Fabio Somenzi
3:30 Symbolic Simulation with Approximate Values
Chris Wilson, David L. Dill, Randal E. Bryant
4:00 Break
4:30 Model Checking Synchronous Timing Diagrams
Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi
5:00 Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
Kiyoharu Hamaguchi, Hidekazu Urushihara, Toshinobu Kashiwabara
7:00 Conference Dinner
                                                    Music! -- Food!! -- Fun!!!
Friday, November 3, 2000
9:00 SAT-Based Image Computation with Application in Reachability Analysis for Verification
Aarti Gupta, Zijiang Yang, Pranav Ashar
10:00 Checking safety properties using induction and a SAT-solver
Mary Sheeran, Satnam Singh, Gunnar Staalmarck
9:30 SAT-based Verification without State Space Traversal
Per Bjesse, Koen Claessen
10:30 Break
11:00 Trends in Computing
Mark E. Dean
11:30 Lunch at Local Restaurants
1:30 Monitor-Based Formal Specification of PCI
Kanna Shimizu, David L. Dill, Alan J. Hu
2:00 Executable Protocol Specification in ESL
E. Clarke, S. German, Y. Lu, H. Veith, D. Wang
2:30 Break
3:00 Speeding Up Image Computation by using RTL Information
Christoph Meinel, Christian Stangier
3:30 Sequential Equivalence Checking by Symbolic Simulation
Gerd Ritter
4:00 Break
4:30 Do you trust your model checker?
Wolfgang Reif, Juergen Ruf, Gerhard Schellhorn, Tobias Vollmer
5:00 B2M: A Semantic Based Tool for BLIF Hardware Descriptions
David Basin, Stefan Friedrich, Sebastian Mödersheim

Document maintained by Steven D. Johnson (sjohnson
posted: 22 September 2000.