@InProceedings{vstte05, author = {Alessandro Coglio and Cordell Green}, title = {A Constructive Approach to Correctness, Exemplified by a Generator for Certified {Java Card} Appplets}, booktitle = {Proc.\ {IFIP} Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE)}, year = {2005}, month = {October}, volume = {4171}, series = {Lecture Notes in Computer Science (LNCS)}, pages = {57--63}, publisher = {Springer} }