An Ivy Formal Verification Installation On Recent Ubuntu

Ivy was introduced in a 2016 PLDI paper “Ivy: Safety Verification by Interactive Generalization“. Ivy helps proof engineers find inductive invariants for proving code safety properties. One of the authors published helpful slides. The code is open sourced under the GPL, with an archived version on Microsoft’s Github, which now directs interested parties to kenmcmil/ivy. […]

DNS Resolver Libraries

We had an application that required parsing received DNS response packets for queries made by other applications. DNS packet structure is a 12-byte header, followed by question entries in the question format, followed by entries in answer, authoritative, and additional sections in the resource record (RR) format. The header specifies the number of entries in each of […]