@article{Mor88,
  author = "C.~C.~Morgan",
  title = "{Auxiliary variables in data refinement}",
  journal = "Information Processing Letters",
  volume = "29",
  number = "6",
  pages = "293--296",
  month = feb,
  year = "1988"
}

@article{Jon92,
  author = "R.~B.~Jones",
  title = "{ICL} {ProofPower}",
  journal = "BCS FACS FACTS",
  volume = "Series III, 1",
  number = "1",
  pages = "10--13",
  year = "1992"
}

@book{WD96,
  title = "{Using Z: Specification, Refinement and Proof}",
  author = "J~.Woodcock and J.~Davis",
  publisher = "Prentice Hall",
  series = "International Series in Computer Science",
  year = "1996",
}

@inproceedings{OB97,
  authors = "W.~R.~Oliveira and R.~S.~M.~Barros",
  title = "{The Real Numbers in Z}",
  booktitle = "Proceedings of the 2nd BCS-FACS Northern Formal Methods
Workshop, Ilkley, 14-15 July 1997",
  publisher = "British Computer Society"
}

@article{CSW03,
  author = "A.~Cavalcanti and A.~Sampaio and J.~Woodcock",
  title = "{A Refinement Strategy for {\Circus}}",
  journal = "Formal Aspects of Computing",
  year = "2003",
  volume = "15",
  number = "2--3",
  pages = "146--181",
  year = "2003"
}

@techreport{Cav08,
  author = "A.~Cavalcanti and P.~Clayton and C.~O'Halloran",
  title = "{From Control Law Diagrams to Ada via {\Circus}}",
  institution = "University of York",
  address = "Heslington, York, YO10 5DD, U.K.",
  month = apr,
  year = "2008"
}

@inproceedings{KHPPTV09,
  author = "T.~Kalibera and J.~Hagelbergand and F.~Pizlo and A.~Plsek and B.~Titzer and J.~Vitek",
  title = "{CDx: A Family of Real-time Java Benchmarks}",
  booktitle = "Proceedings of the 7th International Workshop on Java Technologies for Real-Time and Embedded Systems",
  series = "JTRES 2009",
  publisher = "ACM",
  pages = "41--50",
  month = sep,
  year = "2009"
}

@inproceedings{CWWWZ11,
 author = "A.~Cavalcanti and A.~Wellings and J.~Woodcock and K.~Wei and F.~Zeyda",
 title = "{Safety-Critical Java in {\Circus}}",
 booktitle = "JTRES '11: Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems",
 publisher = "ACM",
 address = "New York, NY, USA",
 month = sep,
 year = "2011"
}

@article{OZC11,
  author = "M. Oliveira and F. Zeyda and A. Cavalcanti",
  title = "{A tactic language for refinement of state-rich concurrent specifications}",
  journal = "Science of Computer Programming",
  volume = "76",
  number = "9",
  pages = "792--833",
  month = sep,
  year = "2011"
}

@article{CCO11,
  author = "A.~Cavalcanti and P.~Clayton and C.~O'Halloran",
  title = "{From control law diagrams to Ada via {\Circus}}",
  journal = "Formal Aspects of Computing",
  publisher = "Springer",
  volume = "23",
  number = "4",
  pages = "465--512",
  month = jul,
  year = "2011"
} 

@article{CWWWZ12,
  author = "A.~Cavalcanti and A.~Wellings and J.~Woodcock and K.~Wei and F.~Zeyda",
  title = "{Development of Safety-Critical Java Programs using {\Circus}}",
  journal = "Concurrency and Copmutation:~Practice and Experience",
  publisher = "ACM",
  month = jun,
  year = "2012",
  note = "Paper submitted for review."
}

@article{ZC12,
  author = "F. Zeyda and M. Oliveira and A. Cavalcanti",
  title = "{Mechanised support for sound refinement tactics}",
  journal = "Formal Aspects of Computing",
  volume = "24",
  number = "1",
  pages = "127--160",
  month = jan,
  year = "2012"
}
