@ARTICLE{Larsen&00,
  KEY           = "Larsen\&00",
  AUTHOR        = "Peter Gorm Larsen, Paul Mukherjee and Kim Sunesen",
  TITLE         = "{Using VDMTools to Model and Validate the Cash 
                    Dispenser Example}",
  JOURNAL       = "Formal Aspects of Computing",
  YEAR          = "2000",
  MONTH         = "December",
  PAGES         = "216-217",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}