Proceedings of Formal Methods in Computer Aided Design, FMCAD 2006
Access full-text files
Date
2006
Authors
Formal Methods in Computer Aided Design
Journal Title
Journal ISSN
Volume Title
Publisher
IEEE
Abstract
Department
Description
Table of Contents: Preface (p. vii) -- Organizing Committee (p. viii) -- Program Committee (p. viii) -- Referees (p. ix) -- HARDWARE VERIFICATION -- Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning / by Jason Baumgartner, IBM Systems; Tilman Glökler, IBM Deutschland; Devi Shanmugam, IBM Systems; Rick Seigler, IBM Systems; Gary Van Huben, IBM Systems; Hari Mony, IBM Systems; Paul Roessler, IBM Systems; and Barinjato Ramanandray, IBM Deutschland (p. 3) -- Post-reboot Equivalence and Compositional Verification of Hardware / by Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, and Ziyad Hanna; Intel, IDC (p. 11) -- Synchronous Elastic Networks / by Sava Krstić, Strategic CAD Labs, Intel; Jordi Cortadella, Universitat Politécnica de Catalunya; Mike Kishinevsky, Strategic CAD Labs, Intel; and John O'Leary, Strategic CAD Labs, Intel (p. 19) -- SAT-BASED METHODS -- Finite Instantiations for Integer Difference Logic / by Hyondeuk Kim and Fabio Somenzi; University of Colorado at Boulder (p. 31) -- Tracking MUSes and Strict Inconsistent Covers / by Éric Grégoire, Bertrand Mazure, and Cédric Piette; Université d’Artois (p. 39) -- Ario: A Linear Integer Arithmetic Logic Solver / by Hossein Sheini and Karem Sakallah; University of Michigan (p. 47) -- Understanding the Dynamic Behaviour of Modern DPLL SAT Solvers through Visual Analysis / by Cameron Brien and Sharad Malik; Princeton University (p. 49) -- SOFTWARE VERIFICATION -- Over-Approximating Boolean Programs with Unbounded Thread Creation / by Byron Cook, Cambridge; Daniel Kroening, ETH Zurich; and Natasha Sharygina, University of Lugano (p. 53) -- An Improved Distance Heuristic Function for Directed Software Model Checking / by Neha Rungta and Eric Mercer; Brigham Young University (p. 60) -- Liveness and Boundedness of Synchronous Data Flow Graphs / by Amir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart Theelen, Mohammad Reza Mousavi, and Sander Stuijk; Eindhoven University of Technology (p. 68) -- Model Checking Data-Dependent Real-Time Properties of the European Train Control System / by Johannes Faber and Roland Meyer; University of Oldenburg (p. 76) -- MODEL CHECKING -- Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee / by Xiaofang Chen, Yu Yang, and Ganesh Gopalakrishnan, University of Utah; and Ching-Tsun Chou, Intel (p. 81) -- Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, and Quantifier Scheduling / by Florian Pigorsch, Christoph Scholl, and Stefan Disch, Albert-Ludwigs-Universität Freiburg (p. 89) -- Symmetry Reduction for STE Model Checking / by Ashish Darbari, Oxford University (p. 97) -- Thorough Checking Revisited / by Shiva Nejati, Mihaela Gheorghiu, and Marsha Chechik, University of Toronto (p. 106) -- AUTOMATA THEORETIC METHODS -- Optimizations for LTL Synthesis / by Barbara Jobstmann and Roderick Bloem, Graz University of Technology (p. 117) -- From PSL to NBA: A Modular Symbolic Encoding / by Alessandro Cimatti, Marco Roveri, and Simone Semprini, ITC-irst; and Stefano Tonetta, University of Lugano (p. 125) -- Assume-Guarantee Reasoning for Deadlock / by Sagar Chaki, Software Engineering Institute; and Nishant Sinha, Carnegie Mellon University (p. 134) -- THEOREM PROVING -- A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification / by Husam Abu-Haimed, Nusym Techology; David Dill, Stanford University; and Sergey Berezin, Synopsys (p. 145) -- An Integration of HOL and ACL2 / by Michael Gordon, University of Cambridge; Warren Hunt and Matt Kaufmann, University of Texas at Austin; and James Reynolds, University of Cambridge (p. 153) -- ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool / by Jun Sawada, IBM Austin Research Laboratory; and Erik Reeber, University of Texas at Austin (p. 161) -- TESTING AND VERIFICATION APPLICATIONS -- Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip / by Claude Helmstetter, Verimag & STMicroelectronics; Florence Maraninchi, Verimag; Laurent Maillet-Contoz, STMicroelectronics; and Matthieu Moy, Verimag (p. 171) -- Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length Operands / by Namrata Shekhar and Priyank Kalla, University of Utah; M. Brandon Meredith and Florian Enescu, Georgia State University (p. 179) -- Design for Verification of the PCI-X Bus / by Ali Habibi, Haja Moinudeen, and Sofiéne Tahar, Concordia University (p. 187) -- Formal Analysis and Verification of an OFDM Modem Design Using HOL / by Abu Nasser Mohammed Abdullah, Concordia University; Behzad Akbarpour, University of Cambridge; and Sofiéne Tahar, Concordia University (p. 189) -- A Formal Model of Lower System Layers / by Julien Schmaltz, Saarland University (p. 191) -- Author Index (p. 193)
12-16 November, 2006 in San Jose, California
12-16 November, 2006 in San Jose, California