|
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 |
