A B model for ensuring soundness of a large subset of the Java card virtual machine
scientific article; zbMATH DE number 1910214