Konrad Slind

Industrial Logician


Dr. Konrad Slind has been a member of the Rockwell Collins Advanced Technology Center since 2009. He has 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 colleagues at NICTA and Cambridge University. 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, and verification of functional programs.

Dr. Slind is currently technical lead on an NSA-sponsored project at Rockwell Collins, with the goal to design and implement the Guardol programming environment. Guardol is aimed at constructing and automatically verifying secure network guards. Guardol programs are given a formal semantics in HOL-4, and guard correctness proofs are automated by verified transformation of proof obligations into a recently invented decision procedure for functional programming. Current research is developing verified generation of guard hardware from specifications in the language of regular expressions.