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)

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

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

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

Synchronous Elastic Networks (Abstract)

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

Finite Instantiations for Integer Difference Logic (Abstract)

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

Tracking MUSes and Strict Inconsistent Covers (Abstract)

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

Ario: A Linear Integer Arithmetic Logic Solver (PDF)

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

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

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

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

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

Liveness and Boundedness of Synchronous Data Flow Graphs (Abstract)

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

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

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

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

Ching-Tsun Chou , Intel Corporation
Xiaofang Chen , University of Utah, USA
Ganesh Gopalakrishnan , University of Utah, USA
Yu Yang , University of Utah, USA
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
Stefan Disch , Albert-Ludwigs-Universitat Freiburg, Institut fur Informatik, Germany
Christoph Scholl , 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)

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

Optimizations for LTL Synthesis (Abstract)

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

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

Stefano Tonetta , University of Lugano, Switzerland
Simone Semprini , ITC-irst
Marco Roveri , ITC-irst
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)

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

An Integration of HOL and ACL2 (Abstract)

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

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

Erik Reeber , University of Texas at Austin, USA
Jun Sawada , IBM Austin Research Laboratory, 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)

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

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

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

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

Sofiene Tahar , Concordia University, Canada
Abu Nasser M. Abdullah , Concordia University, Canada
Behzad Akbarpour , University of Cambridge, UK
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))