Dr. Konrad Slind has been a member of the Trustworthy Methods Group at Collins Aerospace since 2009. He previously worked at the University of Calgary (MSc), Bell Labs Murray Hill (Consultant), Technical University of Munich (PhD), Cambridge University Computer Lab (Post-Doc), and University of Utah School of Computing (faculty). Dr. Slind has led research projects funded by the University of Utah, the NSF, and the NSA.
Slind's research has focused on the theory and application of formal methods. For his MSc work, Slind implemented the HOL (higher order logic) theorem prover in Standard ML. He has developed HOL ever since, lately in collaboration with Michael Norrish at ANU. His PhD work investigated the theory and implementation of general recursion and induction, in both HOL-4 and Isabelle/HOL.
Slind has published in a variety of areas: hardware verification and synthesis, distributed systems, verifying compilation, specification of multiprocessor memory models, verification of cryptographic block ciphers, verification of functional programs.
Dr. Slind is currently working on the DARPA CASE (Cyber Assured Systems Engineering) project. His task is research and development on proof-producing code generation from declarative specifications, in order to build secure message filters and runtime monitors.