@inproceedings{
  Lau:07a,
  author = {K.-K. Lau},
  title = {Using {SPARK} for a Beginner's Course on Reasoning about
  Imperative Programs},
  booktitle = {Proc. 2007 ACM SIGAda Annual International Conference},
  pages = {75-78},
  year = 2007,
  publisher = {ACM}     }