A constructive approach to correctness, exemplified by a generator for certified java card applets

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. © IFIP International Federation for Information Processing 2008.