@TechReport{Rebelo-etal10,
  author =	"Henrique Reb\^{e}lo and Ricardo Lima and Gary T. Leavens 
  and M\'{a}rcio Corn\'{e}lio and Alexandre Mota and C\'{e}sar Oliveira",
  title =	"Optimizing Generated Aspect-Oriented Assertion Checking Code 
  for {JML} Using Programming Laws: An Empirical Study.",
  number =	"CS-TR-10-01",
  series =	"Technical Report",
  address =	"4000 Central Florida Blvd., Orlando, Florida,
		 32816-2362",
  organization = "School of EECS, UCF",
  year = 	"2010",
  month =	feb,
  annote =	"40 references.",
  URL =  	"http://www.eecs.ucf.edu/~leavens/tech-reports/UCF/CS-TR-10-01/TR.pdf",
}