Abstract
We present a constructive approach to correctness and exemplify it by describing a generator for certified Java Card applets that we are building. A proof of full functional correctness is generated, along with the code, from the specification; the proof can be independently checked by a simple proof checker, so that the larger and more complex generator needs not be trusted. We argue that such an approach is a valuable alternative to post-hoc verification, in addressing the Program Verifier Grand Challenge.
Chapter PDF
Similar content being viewed by others
References
Kestrel Institute. AutoSmart, www.kestrel.edu/jcapplets
SRI International. Snark, www.ai.sri.com/~stickel/snark.html
Kestrel Institute and Kestrel Technology LLC. SpecwareTM, www.specware.org
Sun Microsystems. Java Card technology, java.sun.com/javacard
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Coglio, A., Green, C. (2008). A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)