Front matter
1-19
Applications of Hierarchical Verification in Model Checking
Robert Beers, Rajnish Ghughal and Mark Aagaard
20-21
Trends in Computing
Mark E. Dean
22-55
A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon
TM
Processor
David M. Russinoff
56-73
An Algorithm for Strongly Connected Component Analysis in
n
log
n
Symbolic Steps
Roderick Bloem, Harold N. Gabow and Fabio Somenzi
74-91
Automated Refinement Checking for Asynchronous Processes
Rajeev Alur, Radu Grosu and Bow-Yaw Wang
92-109
Border-Block Triangular Form and Conjunction Schedule in Image Computation
In-Ho Moon, Gary D. Hachtel and Fabio Somenzi
110-126
B2M: A Semantic Based Tool for BLIF Hardware Descriptions
David Basin, Stefan Friedrich and Sebastian Mödersheim
127-144
Checking Safety Properties Using Induction and a SAT-Solver
Mary Sheeran, Satnam Singh and Gunnar Stålmarck
145-161
Combining Stream-Based and State-Based Verification Techniques
Nancy A. Day, Mark D. Aagaard and Byron Cook
162-179
A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles
Kavita Ravi, Roderick Bloem and Fabio Somenzi
181-198
Correctness of Pipelined Machines
Panagiotis Manolios
199-216
Do You Trust Your Model Checker?
Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn and Tobias Vollmer
217-236
Executable Protocol Specification in ESL
E. Clarke, S. German, Y. Lu, H. Veith and D. Wang
254-270
Formal Verification of Floating Point Trigonometric Functions
John Harrison
271-282
Hardware Modeling Using Function Encapsulation
Jun Sawada and Warren A. Hunt
283-299
A Methodology for the Formal Analysis of Asynchronous Micropipelines
Antonio Cerone and George J. Milne
300-319
A Methodology for Large-Scale Hardware Verification
Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O’Leary and Carl-Johan H. Seger
320-335
Model Checking Synchronous Timing Diagrams
Nina Amla, E. Allen Emerson, Robert P. Kurshan and Kedar S. Namjoshi
336-352
Model Reductions and a Case Study
Jin Hou and Eduard Cerny
353-371
Modeling and Parameters Synthesis for an Air TrafficManagement System
Adilson Luiz Bonifácio and Arnaldo Vieira Moura
372-390
Monitor-Based Formal Specification of PCI
Kanna Shimizu, David L. Dill and Alan J. Hu
391-408
SAT-Based Image Computation with Application in Reachability Analysis
Aarti Gupta, Zijiang Yang, Pranav Ashar and Anubhav Gupta
409-426
SAT-Based Verification without State Space Traversal
Per Bjesse and Koen Claessen
427-441
Scalable Distributed On-the-Fly Symbolic Model Checking
Shoham Ben-David, Tamir Heyman, Orna Grumberg and Assaf Schuster
442-459
The Semantics of Verilog Using Transition System Combinators
Gordon J. Pace
460-479
Sequential Equivalence Checking by Symbolic Simulation
Gerd Ritter
480-491
Speeding Up Image Computation by Using RTL Information
Christoph Meinel and Christian Stangier
492-506
Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs
Kiyoharu Hamaguchi, Hidekazu Urushihara and Toshinobu Kashiwabara
507-522
Symbolic Simulation with Approximate Values
Chris Wilson, David L. Dill and Randal E. Bryant
523-541
A Theory of Consistency for Modular Synchronous Systems
Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke and Amit Goel
542-556
Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods
Michael Jones and Ganesh Gopalakrishnan
557-574
Visualizing System Factorizations with Behavior Tables
Alex Tsow and Steven D. Johnson
Back matter