112 citations · 279 across the 12 of their papers we have counts for
Showing 2017Show all
2 papers · 1 filter
cs.PL2017★ 23 cited
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…
cs.PL2017★ 112 cited
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi +8
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a sm…