Vale: Verifying high-performance cryptographic assembly code

Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
[ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

26th USENIX Security Symposium (USENIX Security 17)
USENIX Association
Vancouver, BC
Pages 917-934
August 2017
Note(s): ISA specification