The Community for Technology Leaders
Formal Methods in Computer Aided Design (2006)
San Jose, California, USA
Nov. 12, 2006 to Nov. 16, 2006
ISBN: 0-7695-2707-8
TABLE OF CONTENTS
Introduction

Referees (PDF)

pp. ix
Hardware Verification

Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning (Abstract)

Tilman Glokler , IBM Deutschland Entwicklung GmbH
Jason Baumgartner , IBM Systems & Technology Group
Devi Shanmugam , IBM Systems & Technology Group
Rick Seigler , IBM Systems & Technology Group
Gary Van Huben , IBM Systems & Technology Group
Barinjato Ramanandray , IBM Deutschland Entwicklung GmbH
Hari Mony , IBM Systems & Technology Group
Paul Roessler , IBM Systems & Technology Group
pp. 3-10

Post-reboot Equivalence and Compositional Verification of Hardware (Abstract)

Zurab Khasidashvili , Intel, IDC, Israel
Marcelo Skaba , Intel, IDC, Israel
Daher Kaiss , Intel, IDC, Israel
Ziyad Hanna , Intel, IDC, Israel
pp. 11-18

Synchronous Elastic Networks (Abstract)

Sava Krstic , Intel Corporation, USA
Jordi Cortadella , Universitat Politecnica de Catalunya, Spain
Mike Kishinevsky , Intel Corporation, USA
John O?Leary , Intel Corporation, USA
pp. 19-30
SAT-Based Methods

Finite Instantiations for Integer Difference Logic (Abstract)

Hyondeuk Kim , University of Colorado at Boulder, USA
Fabio Somenzi , University of Colorado at Boulder, USA
pp. 31-38

Tracking MUSes and Strict Inconsistent Covers (Abstract)

Eric Gregoire , Universite d?Artois, France
Bertrand Mazure , Universite d?Artois, France
Cedric Piette , Universite d?Artois, France
pp. 39-46

Ario: A Linear Integer Arithmetic Logic Solver (PDF)

Hossein M. Sheini , University of Michigan, USA
Karem A. Sakallah , University of Michigan, USA
pp. 47-48
Software Verification

Over-Approximating Boolean Programs with Unbounded Thread Creation (Abstract)

Byron Cook , Microsoft Research
Daniel Kroening , Computer Systems Institute, ETH, Switzerland
Natasha Sharygina , University of Lugano, Switzerland
pp. 53-59

An Improved Distance Heuristic Function for Directed Software Model Checking (Abstract)

Neha Rungta , Brigham Young University, USA
Eric G Mercer , Brigham Young University, USA
pp. 60-67

Liveness and Boundedness of Synchronous Data Flow Graphs (Abstract)

A.H. Ghamarian , Eindhoven University of Technology, Netherlands
M.C.W. Geilen , Eindhoven University of Technology, Netherlands
T. Basten , Eindhoven University of Technology, Netherlands
B.D. Theelen , Eindhoven University of Technology, Netherlands
M.R. Mousavi , Eindhoven University of Technology, Netherlands
S. Stuijk , Eindhoven University of Technology, Netherlands
pp. 68-75

Model Checking Data-Dependent Real-Time Properties of the European Train Control System (PDF)

Johannes Faber , University of Oldenburg, Germany
Roland Meyer , University of Oldenburg, Germany
pp. 76-77
Model Checking

Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee (Abstract)

Xiaofang Chen , University of Utah, USA
Yu Yang , University of Utah, USA
Ganesh Gopalakrishnan , University of Utah, USA
Ching-Tsun Chou , Intel Corporation
pp. 81-88

Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling (Abstract)

Florian Pigorsch , Albert-Ludwigs-Universitat Freiburg, Institut fur Informatik, Germany
Christoph Scholl , Albert-Ludwigs-Universitat Freiburg, Institut fur Informatik, Germany
Stefan Disch , Albert-Ludwigs-Universitat Freiburg, Institut fur Informatik, Germany
pp. 89-96

Symmetry Reduction for STE Model Checking (Abstract)

Ashish Darbari , Oxford University Computing Lab, UK
pp. 97-105

Thorough Checking Revisited (Abstract)

Shiva Nejati , University of Toronto, Canada
Mihaela Gheorghiu , University of Toronto, Canada
Marsha Chechik , University of Toronto, Canada
pp. 106-116
Automata Theoretic Methods

Optimizations for LTL Synthesis (Abstract)

Barbara Jobstmann , Graz University of Technology
Roderick Bloem , Graz University of Technology
pp. 117-124

From PSL to NBA: a Modular Symbolic Encoding (Abstract)

Marco Roveri , ITC-irst
Simone Semprini , ITC-irst
Stefano Tonetta , University of Lugano, Switzerland
pp. 125-133

Assume-Guarantee Reasoning for Deadlock (Abstract)

Sagar Chaki , Software Engineering Institute
Nishant Sinha , Carnegie Mellon University
pp. 134-144
Theorem Proving

A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification (Abstract)

Husam Abu-Haimed , Nusym Technology, Inc, USA
David L. Dill , Stanford University, USA
Sergey Berezin , Synopsys, Inc, USA
pp. 145-152

An Integration of HOL and ACL2 (Abstract)

Michael J.C. Gordon , University of Cambridge Computer Laboratory, UK
James Reynolds , University of Cambridge Computer Laboratory, UK
Warren A. Hunt , Department of Computer Sciences, USA
Matt Kaufmann , Department of Computer Sciences, USA
pp. 153-160

ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool (Abstract)

Jun Sawada , IBM Austin Research Laboratory, USA
Erik Reeber , University of Texas at Austin, USA
pp. 161-170
Testing and Verification Applications

Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip (Abstract)

C. Helmstetter , Verimag, Centre equation, France; STMicroelectronics, HPC, System Platform Group, France
F. Maraninchi , Verimag, Centre equation, France
L. Maillet-Contoz , STMicroelectronics, HPC, System Platform Group, France
M. Moy , Verimag, Centre equation, France
pp. 171-178

Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands (Abstract)

Namrata Shekhar , University of Utah, USA
Priyank Kalla , University of Utah, USA
M. Brandon Meredith , Georgia State University, USA
Florian Enescu , Georgia State University, USA
pp. 179-186

Design for Verification of the PCI-X Bus (PDF)

Haja Moinudeen , Concordia University, Canada
Ali Habibi , Concordia University, Canada
Sofiene Tahar , Concordia University, Canada
pp. 187-188

Formal Analysis and Verification of an OFDM Modem Design using HOL (PDF)

Abu Nasser M. Abdullah , Concordia University, Canada
Behzad Akbarpour , University of Cambridge, UK
Sofiene Tahar , Concordia University, Canada
pp. 189-190

A Formal Model of Lower System Layers (PDF)

Julien Schmaltz , Saarland University, Germany
pp. 191-192
Author Index

Author Index (PDF)

pp. 193
83 ms
(Ver 3.3 (11022016))