kai-e.github.io

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

tba (currently my recent work is sequestered in ARM, QualComm, or Ghost Autonomy IP)

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.

Formalisations and proofs of problems, e.g., from the “100 list” in PVS.

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)

This site is open source. Improve this page.