Mr. Grant Jurgensen is a Computer Scientist at Kestrel Institute and Kestrel Technology LLC. He is currently working primarily on infrastructure to support formal derivations of C code from ACL2 specifications using ATC. He is interested in formal methods, programming language theory, and type theory.
Before joining Kestrel Institute, Grant Jurgensen worked as a graduate research assistant at the University of Kansas, where he was advised by Dr. Perry Alexander. There, he was involved in the design and implementation of Copland, a domain-specific language for specifying remote attestations. He led the development of an attestation manager based on Copland, as well as designed a system architecture to support trustworthy remote attestation. Finally, he modelled and verified aspects of said system within the Coq theorem prover .
He graduated with a Master’s degree in Computer Science from the University of Kansas in May, 2022.
Jurgensen, G. A Verified Architecture for Trustworthy Remote Attestation . Master’s thesis, University of Kansas. April, 2022.
Petz, A., Jurgensen, G., and Alexander, P. Design and Formal Verification of a Copland-based Attestation Protocol . In ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'21), Virtual, Nov 20-22, 2021.