6. FMCAD 2006: San Jose, California, USA

Hardware Verification

• Tilman Glökler, Jason Baumgartner, Devi Shanmugam, A. E. (Rick) Seigler, Gary A. Van Huben, Barinjato Ramanandray, Hari Mony, Paul Roessler:
  Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning. 3-10
  
• Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna:
  Post-reboot Equivalence and Compositional Verification of Hardware. 11-18
  
• Sava Krstic, Jordi Cortadella, Michael Kishinevsky, John O'Leary:
  Synchronous Elastic Networks. 19-30
  

SAT-Based Methods

• Hyondeuk Kim, Fabio Somenzi:
  Finite Instantiations for Integer Difference Logic. 31-38
  
• Éric Grégoire, Bertrand Mazure, Cédric Piette:
  Tracking MUSes and Strict Inconsistent Covers. 39-46
  
• Hossein M. Sheini, Karem A. Sakallah:
  Ario: A Linear Integer Arithmetic Logic Solver. 47-48
  
• Cameron Brien, Sharad Malik:
  Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis. 49-50
  

Software Verification

• Byron Cook, Daniel Kroening, Natasha Sharygina:
  Over-Approximating Boolean Programs with Unbounded Thread Creation. 53-59
  
• Neha Rungta, Eric G. Mercer:
  An Improved Distance Heuristic Function for Directed Software Model Checking. 60-67
  
• Amir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart D. Theelen, Mohammad Reza Mousavi, Sander Stuijk:
  Liveness and Boundedness of Synchronous Data Flow Graphs. 68-75
  
• Johannes Faber, Roland Meyer:
  Model Checking Data-Dependent Real-Time Properties of the European Train Control System. 76-77
  

Model Checking

• Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou:
  Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee. 81-88
  
• Florian Pigorsch, Christoph Scholl, Stefan Disch:
  Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling. 89-96
  
• Ashish Darbari:
  Symmetry Reduction for STE Model Checking. 97-105
  
• Shiva Nejati, Mihaela Gheorghiu, Marsha Chechik:
  Thorough Checking Revisited. 106-116
  

Automata Theoretic Methods

• Barbara Jobstmann, Roderick Bloem:
  Optimizations for LTL Synthesis. 117-124
  
• Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta:
  From PSL to NBA: a Modular Symbolic Encoding. 125-133
  
• Sagar Chaki, Nishant Sinha:
  Assume-Guarantee Reasoning for Deadlock. 134-144
  

Theorem Proving

• Husam Abu-Haimed, David L. Dill, Sergey Berezin:
  A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification. 145-152
  
• Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann:
  An Integration of HOL and ACL2. 153-160
  
• Jun Sawada, Erik Reeber:
  ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. 161-170
  

Testing and Verification Applications

• C. Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, Matthieu Moy:
  Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip. 171-178
  
• Namrata Shekhar, Priyank Kalla, M. Brandon Meredith, Florian Enescu:
  Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands. 179-186
  
• Haja Moinudeen, Ali Habibi, Sofiène Tahar:
  Design for Verification of the PCI-X Bus. 187-188
  
• Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofiène Tahar:
  Formal Analysis and Verification of an OFDM Modem Design using HOL. 189-190
  
• Julien Schmaltz:
  A Formal Model of Lower System Layers. 191-192