52 citations · 52 across the 1 of their papers we have counts for
2 papers
cs.PL2018
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li +6
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie toge…
cs.CR2017★ 52 cited
Verified Correctness and Security of mbedTLS HMAC-DRBG
Katherine Q. Ye, Matthew Green, Naphat Sanguansin +3
We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security--that its output is pseudorandom--using a hybrid game-bas…