2. FMCAD 1998: Palo Alto, California, USA

@proceedings{DBLP:conf/fmcad/1998,
  editor    = {Ganesh Gopalakrishnan and
               Phillip J. Windley},
  title     = {Formal Methods in Computer-Aided Design, Second International
               Conference, FMCAD '98, Palo Alto, California, USA, November 4-6,
               1998, Proceedings},
  booktitle = {FMCAD},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1522},
  year      = {1998},
  isbn      = {3-540-65191-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

• Kenneth L. McMillan:
  Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract). 1
  
• Robert B. Jones, Jens U. Skakkebæk, David L. Dill:
  Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution. 2-17
  
• Miroslav N. Velev, Randal E. Bryant:
  Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. 18-35
  
• M. Oliver Möller, Harald Rueß:
  Solving Bit-Vector Equations. 36-48
  
• Ásgeir Th. Eiríksson:
  The Formal Design of 1M-gate ASICs. 49-63
  
• Justin E. Harlow III, Franc Brglez:
  Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations. 64-81
  
• Mary Sheeran, Gunnar Stålmarck:
  A Tutorial on Stålmarcks's Proof Procedure for Propositional Logic. 82-99
  
• Macha Nikolskaïa, Antoine Rauzy, David James Sherman:
  Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods. 100-114
  
• Kathi Fisler, Moshe Y. Vardi:
  Bisimulation Minimization in an Automata-Theoretic Verification Framework. 115-132
  
• F. Keith Hanna:
  Automatic Verification of Mixed-Level Logic Circuits. 133-166
  
• Fen Jin, Henrik Hulgaard, Eduard Cerny:
  Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints. 167-184
  
• Jürgen Ruf, Thomas Kropf:
  Using MTBDDs for Compostion and Model Checking of Real-Time Systems. 185-202
  
• Carl-Johan H. Seger:
  Formal Methods in CAD from an Industrial Perspective (abstract). 203
  
• Nazanin Mansouri, Ranga Vemuri:
  A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool. 204-221
  
• Thomas Lock, Michael Mendler, Matthias Mutz:
  Combined Formal Post- and Presynthesis Verification in High Level Synthesis. 222-236
  
• Abdelillah Mokkedem, Ravi Hosabettu, Ganesh Gopalakrishnan:
  Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. 237-254
  
• Bwolen Yang, Randal E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, Fabio Somenzi:
  A Performance Study of BDD-Based Model Checking. 255-289
  
• Gila Kamhi, Limor Fix, Ziv Binyamini:
  Symbolic Model Checking Visualization. 290-303
  
• Sela Mador-Haim, Limor Fix:
  Input Elimination and Abstraction in Model Checking. 304-320
  
• David A. Greve:
  Symbolic Simulation of the JEM1 Microprocessor. 321-333
  
• J. Strother Moore:
  Symbolic Simulation: An ACL2 Approach. 334-350
  
• Amir Pnueli, Tamarah Arons:
  Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study. 351-368
  
• Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu:
  Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. 369-386
  
• Jeffrey X. Su, David L. Dill, Jens U. Skakkebæk:
  Formally Verifying Data and Control with Weak Reachability Invariants. 387-402
  
• C. Norris Ip:
  Generalized Reversible Rules. 403-420
  
• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
  An Assume-Guarantee Rule for Checking Simulation. 421-432
  
• Sofiène Tahar, Paul Curzon, Jianping Lu:
  Three Approaches to Hardware Verification: HOL, MDG and VIS Compared. 433-450
  
• Shiu-Kai Chin, Jang Dae Kim:
  An Instruction Set Process Calculus. 451-468
  
• James H. Kukula, Thomas R. Shiple, Adnan Aziz:
  Techniques for Implicit State Enumeration of EFSMs. 469-482
  
• Klaus Schneider:
  Model Checking on Product Structures. 483-500
  
• Kim Milvang-Jensen, Alan J. Hu:
  BDDNOW: A Parallel BDD Package. 501-507
  
• David Déharbe, Subash Shankar, Edmund M. Clarke:
  Model Checking VHDL with CV. 508-514
  
• Annette Bunker, Trent N. Larson, Michael D. Jones, Phillip J. Windley:
  Alexandria: A Tool for Hierarchical Verification. 515-522
  
• Ratan Nalumasu, Ganesh Gopalakrishnan:
  PV: An Explicit Enumeration Model-Checker. 523-528
  

Last update Tue Feb 14 03:56:06 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page