Correct hardware design and verification methods [electronic resource] : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001 : proceedings / Tiziana Margaria, Tom Melham (eds.).
- Conference Author:
- CHARME 2001 (2001 : Livingston, Scotland)
- Published:
- Berlin ; New York : Springer, [2001]
- Copyright Date:
- ©2001
- Physical Description:
- xii, 482 pages : illustrations ; 24 cm.
- Additional Creators:
- Margaria-Steffen, Tiziana, 1964-
Melham, T. F. (Tom F.) - Access Online:
- serialssolutions.com
- Series:
- Lecture notes in computer science, 2144
- Restrictions on Access:
- License restrictions may limit access.
- Contents:
- Machine generated contents note: View from the Fringe of the Fringe (Extended Summary) / Steven D. Johnson -- Hardware Synthesis Using SAFL and Application to Processor Design / Alan Mycroft / Richard Sharp -- Applications of Hierarchical Verification in Model Checking / Mark Aagaard / Robert Beers / Rajnish Ghughal -- Pruning Techniques for the SAT-Based Bounded Model Checking Problem / Ofer Shtrichman -- Heuristics for Hierarchical Partitioning with Application to Model Checking / M. Oliver Moller / Rajeev Alur -- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs / Dirk Beyer -- Deriving Real-Time Programs from Duration Calculus Specifications / Dang Van Hung / Francois Siewe -- Reproducing Synchronization Bugs with Model Checking / Sagi Katz / Ron Kiper / Karen Yorav -- Formally-Based Design Evaluation / Kenneth J. Turner / Ji He -- Multiclock Esterel / Ellen Sentovich / Gerard Berry -- Register Transformations with Multiple Clock Domains / Alvin R. Albrecht / Alan J. Hu -- Temporal Properties of Self-Timed Rings / Mark Greenstreet / Anthony Winstanley -- Coverability Analysis Using Symbolic Model Checking / Shmuel Ur / Yaron Wolfsthal / Gil Ratzaby -- Specifying Hardware Timing with ET-Lotos / Ji He / Kenneth J. Turner -- Formal Pipeline Design / Juha Plosila / Tiberiu Seceleanu -- Verification of Basic Block Schedules Using RTL Transformations / Rajesh Radhakrishnan / Elena Teica / Ranga Vemuri -- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking / K. L. McMillan -- Proof Engineering in the Large: Formal Verification of Pentium 4 Floating-Point Divider / Roope Kaivola / Katherine Kohatsu -- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques / Steve McKeever / Wayne Luk -- A Higher-Level Language for Hardware Synthesis / Richard Sharp / Alan Mycroft -- Hierarchical Verification Using an MDG-HOL Hybrid Tool / Sofiene Tahar / Iskander Kort / Paul Curzon -- Exploiting Transition Locality in Automatic Verification / [et al.] / Giuseppe Della Penna / Enrico Tronci / Benedetto Intrigila -- Efficient Debugging in a Formal Verification Environment / Fady Copty / Amitai Irron / Osnat Weissberg / [et al.] -- Using Combinatorial Optimization Methods for Quantification Scheduling / P. Chauhan / E. Clarke / S. Jha / [et al.] -- Net Reductions for LTL Model-Checking / Claus Schroter / Javier Esparza -- Formal Verification of the VAMP Floating Point Unit / Christian Jacobi / Christoph Berg -- A Specification Methodology by a Collection of Compact Properties as Applied to the Intel Itanium Processor Bus Protocol / Ching-Tsun Chou / Kanna Shimizu / David L. Dill -- The Design and Verification of a Sorter Core / Koen Claessen / Satnam Singh / Mary Sheeran -- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems for Chip / Xiaohua Kong / Larry Weidong Ying / Radu Negulescu -- Using Abstract Specifications to Verify PowerPC Custom Memories by Symbolic Trajectory Evaluation / Andrew Martin / [et al.] / Jacob Abraham / Jayanta Bhadra -- Formal Verification of Conflict Detection Algorithms / Ricky Butler / Victor Carreno / Gilles Dowek / [et al.] -- Induction-Oriented Formal Verification in Symmetric Interconnection Networks / Laurence Pierre / Eric Gascard -- A Framework for Microprocessor Correctness Statements / Byron Cook / [et al.] / Nancy A. Day / Mark D. Aagaard -- From Operational Semantics to Denotational Semantics for Verilog / Zhu Huibiao / Jonathan P. Bowen / He Jifeng -- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming / Li Xuandong / [et al.] / Pei Yu / Zhao Jianhua.
- Subject(s):
- Genre(s):
- ISBN:
- 3540425411 (pbk. : alk. paper)
- Bibliography Note:
- Includes bibliographical references and index.
View MARC record | catkey: 7808002