10. CHARME 1999: Bad Herrenalp, Germany

@proceedings{DBLP:conf/charme/1999,
  editor    = {Laurence Pierre and
               Thomas Kropf},
  title     = {Correct Hardware Design and Verification Methods, 10th IFIP WG
               10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb,
               Germany, September 27-29, 1999, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1703},
  year      = {1999},
  isbn      = {3-540-66559-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Talks

• Gérard Berry:
  Esterel and Jazz: Two Synchronous Languages for Circuit Design (Abstract). 1
  Electronic Edition (Springer LINK) BibTeX
• Peter Jansen:
  Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specification. 2-7
  Electronic Edition (Springer LINK) BibTeX

Proof of Microprocessors

• Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas:
  A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. 8-22
  Electronic Edition (Springer LINK) BibTeX
• Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz:
  Formal Verification of Explicitly Parallel Microprocessors. 23-36
  Electronic Edition (Springer LINK) BibTeX
• Miroslav N. Velev, Randal E. Bryant:
  Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. 37-53
  Electronic Edition (Springer LINK) BibTeX

Model Checking

• Yuan Yu, Panagiotis Manolios, Leslie Lamport:
  Model Checking TLA⁺ Specifications. 54-66
  Electronic Edition (Springer LINK) BibTeX
• Nina Amla, E. Allen Emerson, Kedar S. Namjoshi:
  Efficient Decompositional Model Checking for Regular Timing Diagrams. 67-81
  Electronic Edition (Springer LINK) BibTeX
• Orna Kupferman, Moshe Y. Vardi:
  Vacuity Detection in Temporal Model Checking. 82-96
  Electronic Edition (Springer LINK) BibTeX

Formal Methiods and Industrial Applications

• Cindy Eisner:
  Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. 97-109
  Electronic Edition (Springer LINK) BibTeX
• Ying Xu, Eduard Cerny, Allan Silburt, A. Coady, Ying Liu, Philip Pownall:
  Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors. 110-124
  Electronic Edition (Springer LINK) BibTeX
• Marius Bozga, Oded Maler, Stavros Tripakis:
  Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics. 125-141
  Electronic Edition (Springer LINK) BibTeX

Abstraction and Compositional Techniques

• E. Allen Emerson, Richard J. Trefler:
  From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. 142-156
  Electronic Edition (Springer LINK) BibTeX
• Dirk W. Hoffmann, Thomas Kropf:
  Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction. 157-171
  Electronic Edition (Springer LINK) BibTeX
• Edmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang:
  Abstract BDDs: A Technque for Using Abstraction in Model Checking. 172-186
  Electronic Edition (Springer LINK) BibTeX

Theorem Proving Related Approaches

• Christian Blumenröhr, Viktor K. Sabelfeld:
  Formal Synthesis at the Algorithmic Level. 187-201
  Electronic Edition (Springer LINK) BibTeX
• Mark Aagaard, Thomas F. Melham, John W. O'Leary:
  Xs are for Trajectory Evaluation, Booleans are for Theorem Proving. 202-218
  Electronic Edition (Springer LINK) BibTeX
• Kenneth L. McMillan:
  Verification of Infinite State Systems by Compositional Model Checking. 219-234
  Electronic Edition (Springer LINK) BibTeX

Symbolic Simulation/Symbolic Traversal

• Gerd Ritter, Hans Eveking, Holger Hinrichsen:
  Formal Verification of Designs with Complex Control by Symbolic Simulation. 234-249
  Electronic Edition (Springer LINK) BibTeX
• Kavita Ravi, Fabio Somenzi:
  Hints to accelerate Symbolic Traversal. 250-264
  Electronic Edition (Springer LINK) BibTeX

Specification Languages and Methodologies

• Jürgen Ruf, Thomas Kropf:
  Modleing and Checking Networks of Communicating Real-Time Process. 265-279
  Electronic Edition (Springer LINK) BibTeX
• Sagi Katz, Orna Grumberg, Daniel Geist:
  "Have I written enough Properties?" - A Method of Comparison between Specification and Implementation. 280-297
  Electronic Edition (Springer LINK) BibTeX
• Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum:
  Program Slicing of Hardware Description Languages. 298-312
  Electronic Edition (Springer LINK) BibTeX

Posters

• Jun Sawada, Warren A. Hunt Jr.:
  Results of the Verification of a Complex Pipelined Machine Model. 313-316
  Electronic Edition (Springer LINK) BibTeX
• Hüsnü Yenigün, Vladimir Levin, Doron Peled, Peter A. Beerel:
  Hazard-Freedom Checking in Speed-Independent Systems. 317-320
  Electronic Edition (Springer LINK) BibTeX
• Klaus Schneider:
  Yet another Look at the LTL Model Checking. 321-325
  Electronic Edition (Springer LINK) BibTeX
• Stefan Hendricx, Luc J. M. Claesen:
  Verification of Finite-State-Machine Refinements Using a Symbolic Methodology. 326-329
  Electronic Edition (Springer LINK) BibTeX
• George Economakos, George K. Papakonstantinou:
  Refinement and Property Checking in High-Level Synthesis using Attribute Grammars. 330-333
  Electronic Edition (Springer LINK) BibTeX
• Steven D. Johnson, Yanhong A. Liu, Yuchen Zhang:
  A Systematic Incrementalization Technique and Its Application to Hardware Design. 334-337
  Electronic Edition (Springer LINK) BibTeX
• Kathi Fisler, Moshe Y. Vardi:
  Bisimulation and Model Checking. 338-341
  Electronic Edition (Springer LINK) BibTeX
• Kenneth L. McMillan:
  Circular Compositional Reasoning about Liveness. 342-345
  Electronic Edition (Springer LINK) BibTeX
• Nancy A. Day, Jeffrey R. Lewis, Byron Cook:
  Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. 346-349
  Electronic Edition (Springer LINK) BibTeX
• Aarti Gupta, Pranav Ashar, Sharad Malik:
  Exploiting Retiming in a Guided Simulation Based Validation Methodology. 350-353
  Electronic Edition (Springer LINK) BibTeX
• Jens Chr. Godesken:
  Fault Models for Embedded Systems (Extended Abstract). 354-359
  Electronic Edition (Springer LINK) BibTeX
• Klaus Schneider, Michaela Huhn, George Logothetis:
  Validation of Object-Oriented Concurrent Designs by Model Checking. 360-364
  Electronic Edition (Springer LINK) BibTeX