C. Averill

Formally-Verified, Tight Timing Constraints for Machine Code

Cloq is introduced, the first dependently typed, machine-checked framework for verifying timing properties of raw (stripped) machine code within the Rocq interactive theorem-proving environment, and provides high-assurance, high-precision timing guarantees that verify that real-time systems and cryptographic algorithms...