The programming of critical systems, where human life or critical infrastructure is at stake, necessitates correctness as- surances of a kind different than what we are used to in general-purpose programming. We describe an experimental attempt at verification of Small- talk VM using mechanized proof. Only the native code gen- eration part is verified. The generator is developed in the Coq proof assistant and is largely based on the CompCert compiler backend. The resulting VM successfully runs the ANSI test suite on a number of targets with different ISAs.
The paper is available from ACM or the final draft is available locally.
