11th Advanced Research Working Conference
on Correct Hardware Design and Verification Methods

4-7 September 2001
Institute for System Level Integration
Livingston, Scotland.

CHARME 2001 Advance Programme

The CHARME 2001 scientific programme begins on the afternoon of Tuesday the 4th of September and runs through to the end of the afternoon on Friday the 7th of September. A joint session with TPHOLs 2001 takes place on Wednesday 5 September in Edinburgh. On the morning of Tuesday the 4th of September there is a small programme of tutorials associated with the conference.

Detailed Programme Information

• Tutorials: See the tutorials web page for details of the tutorial programme.
• Programme: The full scientific programme is available on the information for participants page.

Tutorials

• Robert Fairlie, Verilab Ltd.
  A Practical Approach to Verification in SoC Design

• Gérard Berry, Esterel Technologies
  High-level Description, Synthesis, and Validation of Control-Dominated Designs

Full Papers

• Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones
  A Framework for Microprocessor Correctness Statements
• Alvin R. Albrecht and Alan J. Hu
  Register Transformations with Multiple Clock Domains
• Christoph Berg and Christian Jacobi
  Formal Verification of the VAMP Floating Point Unit
• Gérard Berry and Ellen Sentovich
  Multiclock Esterel
• Jayanta Bhadra, Andrew Martin, Jacob Abraham, and Magdy Abadir
  Using Abstract Specifications to Verify PowerPC Custom Memories by Symbolic Trajectory Evaluation
• Ricky Butler, Víctor Carreño, Gilles Dowek, and César Muñoz
  Formal Verification of Conflict Detection Algorithms
• Pankajkumar Chauhan, E. Clarke, S. Jha, J. Kukula, H. Veith, and D. Wang
  Using Combinatorial Optimization Methods for Quantification Scheduling
• Koen Claessen, Mary Sheeran, and Satnam Singh
  The Design and Verification of a Sorter Core
• Fady Copty, Amitai Irron, Osnat Weissberg, Nathan Kropp, and Gila Kamhi
  Efficient Debugging in a Formal Verification Environment
• Javier Esparza and Claus Schröter
  Net Reductions for LTL Model-Checking
• Eric Gascard and Laurence Pierre
  Induction-Oriented Formal Verification in Symmetric Interconnection Networks
• Zhu Huibiao, Jonathan P. Bowen, and He Jifeng
  From Operational Semantics to Denotational Semantics for Verilog
• Roope Kaivola and Katherine Kohatsu
  Proof Engineering in the Large: Formal Verification of Pentium 4 Floating-Point Divider
• Xiaohua Kong, Radu Negulescu, and Larry Weidong Ying
  Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip
• Iskander Kort, Sofiene Tahar, and Paul Curzon
  Hierarchical Verification Using an MDG-HOL Hybrid Tool
• Steve McKeever and Wayne Luk
  Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques
• K. L. McMillan
  Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
• M. Oliver Möller and Rajeev Alur
  Heuristics for Hierarchical Partitioning with Application to Model Checking
• Richard Sharp and Alan Mycroft
  A Higher Level Language for Hardware Synthesis
• Kanna Shimizu, David L. Dill, Ching-Tsun Chou
  A Specification Methodology by a Collection of Compact Properties as Applied to the Intel Itanium Processor Bus Protocol
• Ofer Shtrichman
  Pruning Techniques for the SAT-based Bounded Model Checking Problem
• Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, and Marisa Venturini Zilli
  Exploiting Transition Locality in Automatic Verification
• Anthony Winstanley and Mark Greenstreet
  Temporal Properties of Self-Timed Rings
• Li Xuandong, Pei Yu, Zhao Jianhua, Li Yong, Zheng Tao, and Zheng Guoliang
  Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming

Short Papers

• Dirk Beyer
  Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs
• Ji He and Kenneth J. Turner
  Specifying Hardware Timing with ET-LOTOS
• Rajesh Radhakrishnan, Elena Teica, and Ranga Vemuri
  Verification of Basic Block Schedules Using RTL Transformations
• Gil Ratzaby, Shmuel Ur, and Yaron Wolfsthal
  Coverability Analysis Using Symbolic Model Checking
• Tiberiu Seceleanu and Juha Plosila
  Formal Pipeline Design
• François Siewe and Dang Van Hung
  Deriving Real-Time Programs from Duration Calculus Specifications
• Kenneth J. Turner and Ji He
  Formally-Based Design Evaluation
• Karen Yorav, Sagi Katz, and Ron Kiper
  Reproducing Synchronization Bugs with Model Checking