@conference {DBLP:conf/nfm/Herencia-ZapanaJOGFPA12,
	title = {PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL},
	booktitle = {NASA Formal Methods},
	year = {2012},
	author = {Heber Herencia-Zapana and Romain Jobredeaux and Sam Owre and Pierre-Loic Garoche and Eric M. Feron and Gilberto Perez and Pablo Ascariz}
}