11. CHARME 2001: Livingston, Scotland, UK

Invited Contributions

• Steven D. Johnson:
  View from the Fringe of the Fringe. 1-12
  
• Alan Mycroft, Richard Sharp:
  Hardware Synthesis Using SAFL and Application to Processor Design. 13-39
  

FMCAD 2000

• Robert Beers, Rajnish Ghughal, Mark Aagaard:
  Applications of Hierarchical Verification in Model Checking. 40-57
  

Model Checking 1

• Ofer Strichman:
  Pruning Techniques for the SAT-Based Bounded Model Checking Problem. 58-70
  
• M. Oliver Möller, Rajeev Alur:
  Heuristics for Hierarchical Partitioning with Application to Model Checking. 71-85
  

Short Papers 1

• Dirk Beyer:
  Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs. 86-91
  
• François Siewe, Dang Van Hung:
  Deriving Real-Time Programs from Duration Calculus Specifications. 92-97
  
• Karen Yorav, Sagi Katz, Ron Kiper:
  Reproducing Synchronization Bugs with Model Checking. 98-103
  
• Kenneth J. Turner, Ji He:
  Formally-Based Design Evaluation. 104-109
  

Clocking Issues

• Gérard Berry, Ellen Sentovich:
  Multiclock Esterel. 110-125
  
• Alvin R. Albrecht, Alan J. Hu:
  Register Transformations with Multiple Clock Domains. 126-139
  
• Anthony Winstanley, Mark R. Greenstreet:
  Temporal Properties of Self-Timed Rings. 140-154
  

Short Papers 2

• Gil Ratsaby, Shmuel Ur, Yaron Wolfsthal:
  Coverability Analysis Using Symbolic Model Checking. 155-160
  
• Ji He, Kenneth J. Turner:
  Specifying Hardware Timing with ET-L OTOS. 161-166
  
• Tiberiu Seceleanu, Juha Plosila:
  Formal Pipeline Design. 167-172
  
• Rajesh Radhakrishnan, Elena Teica, Ranga Vemuri:
  Verification of Basic Block Schedules Using RTL Transformations. 173-178
  

Joint Session with TPHOLs

• Kenneth L. McMillan:
  Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. 179-195
  
• Roope Kaivola, Katherine R. Kohatsu:
  Proof Engineering in the Large: Formal Verification of Pentium^® 4 Floating-Point Divider. 196-211
  

Hardware Compilation

• Steve McKeever, Wayne Luk:
  Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques. 212-227
  
• Richard Sharp, Alan Mycroft:
  A Higher-Level Language for Hardware Synthesis. 228-243
  

Tools

• Iskander Kort, Sofiène Tahar, Paul Curzon:
  Hierarchical Verification Using an MDG-HOL Hybrid Tool. 244-258
  
• Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, Marisa Venturini Zilli:
  Exploiting Transition Locality in Automatic Verification. 259-274
  
• Fady Copty, Amitai Irron, Osnat Weissberg, Nathan P. Kropp, Gila Kamhi:
  Efficient Debugging in a Formal Verification Environment. 275-292
  

Model Checking 2

• Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang:
  Using Combinatorial Optimization Methods for Quantification Scheduling. 293-309
  
• Javier Esparza, Claus Schröter:
  Net Reductions for LTL Model-Checking. 310-324
  

Component Verification

• Christoph Berg, Christian Jacobi:
  Formal Verification of the VAMP Floating Point Unit. 325-339
  
• Kanna Shimizu, David L. Dill, Ching-Tsun Chou:
  A Specification Methodology by a Collection of Compact Properties as Applied to the Intel^® Itanium^TM Processor Bus Protocol. 340-354
  
• Koen Claessen, Mary Sheeran, Satnam Singh:
  The Design and Verification of a Sorter Core. 355-369
  

Case Studies

• Xiaohua Kong, Radu Negulescu, Larry Weidong Ying:
  Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip. 370-385
  
• Jayanta Bhadra, Andrew K. Martin, Jacob A. Abraham, Magdy S. Abadir:
  Using Abstract Specifications to Verify PowerPC^TM Custom Memories by Symbolic Trajectory Evaluation. 386-402
  

Algorithm Verification

• Ricky W. Butler, Victor Carreño, Gilles Dowek, César A. Muñoz:
  Formal Verification of Conflict Detection Algorithms. 403-417
  
• Eric Gascard, Laurence Pierre:
  Induction-Oriented Formal Verification in Symmetric Interconnection Networks. 418-432
  
• Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones:
  A Framework for Microprocessor Correctness Statements. 433-448
  

Duration Calculus

• Huibiao Zhu, Jonathan P. Bowen, Jifeng He:
  From Operational Semantics to Denotational Semantics for Verilog. 449-466
  
• Xuandong Li, Yu Pei, Jianhua Zhao, Yong Li, Tao Zheng, Guoliang Zheng:
  Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming. 465-480
  

Last update Mon May 20 22:35:13 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page