11. CHARME 2001: Livingston, Scotland, UK

@proceedings{DBLP:conf/charme/2001,
  editor    = {Tiziana Margaria and
               Thomas F. Melham},
  title     = {Correct Hardware Design and Verification Methods, 11th IFIP WG
               10.5 Advanced Research Working Conference, CHARME 2001, Livingston,
               Scotland, UK, September 4-7, 2001, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2144},
  year      = {2001},
  isbn      = {3-540-42541-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Contributions

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

FMCAD 2000

• Robert Beers, Rajnish Ghughal, Mark Aagaard:
  Applications of Hierarchical Verification in Model Checking. 40-57
  Electronic Edition (Springer LINK) BibTeX

Model Checking 1

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

Short Papers 1

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

Clocking Issues

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

Short Papers 2

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

Joint Session with TPHOLs

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

Hardware Compilation

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

Tools

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

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
  Electronic Edition (Springer LINK) BibTeX
• Javier Esparza, Claus Schröter:
  Net Reductions for LTL Model-Checking. 310-324
  Electronic Edition (Springer LINK) BibTeX

Component Verification

• Christoph Berg, Christian Jacobi:
  Formal Verification of the VAMP Floating Point Unit. 325-339
  Electronic Edition (Springer LINK) BibTeX
• 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
  Electronic Edition (Springer LINK) BibTeX
• Koen Claessen, Mary Sheeran, Satnam Singh:
  The Design and Verification of a Sorter Core. 355-369
  Electronic Edition (Springer LINK) BibTeX

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
  Electronic Edition (Springer LINK) BibTeX
• 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
  Electronic Edition (Springer LINK) BibTeX

Algorithm Verification

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

Duration Calculus

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