Formal Verification of a JavaCard Virtual Machine with Frama-C. - Adel Djoudi; Martin Hána; Nikolai Kosmatov (FM, 2021)