Rui Fernandes
Researcher at the Max Planck Institute for Security and Privacy (MPI-SP)
Correctness Proofs of Jasmin Programs: Part 1 - Overview
This is the first post in a series on how to prove that Jasmin are correct with respect to a high-level specification written in EasyCrypt.