Kai
Kai Engelhardt’s personal public space
Work
As a verification architect I
- devise roadmaps for building trustworthy systems,
- re-discover or create verification techniques tailored to these roadmaps,
- design and implement tool prototypes to aid in executing roadmaps, and
- foster an engineering culture where trustworthiness of the product is a key ingredient.
This often means I do things somewhat differently. If that is the case and the cost/benefit trade-off looks promising, I help with educating engineers how to do things differently, too.
Pubs
See google scholar, dblp, or my local list.
Recent presentations include
- “Update on the adoption of synchronous languages at gh.st”, Synchron 2020, slides
- “Adventures in Verification Land for Glorified Ring Buffers”, Synchron 2021, slides
- “Neural Net Validation - classical CS and high school maths to the rescue”, Synchron 2021, slides
Errata for the data refinement book: pdf.
Specs/Code/Proofs
Most recent work is sequestered in ARM, QualComm, or Ghost Autonomy IP.
Formalisations and proofs of problems, e.g., from the “100 list” in PVS.
Misc
News 2023/05/03: The 2022 iteration of the ACM Software System Award goes to our team of authors of seL4: formal verification of an OS kernel.
News 2023/04/03: Build instructions for PVS on ARM Macs.
Contact
Email & Messages.app: k <digit one> k <digit two> t <at> icloud <dot> com (even the old kaie <at> cse <dot> unsw <dot> edu <dot> au could still work)