Dr. Gacek is a Senior Industrial Logician at the Rockwell Collins Advanced Technology Center. He has a particular interest in developing tools for the application of formal methods. He created the Abella theorem prover, an interactive theorem prover based on lambda-tree syntax. He also created JKind, an infinite-state model checker for safety properties. Dr. Gacek developed various other tools and languages that are in use both inside and outside of Rockwell Collins. His broader interests include theorem proving, model checking, language translation, software design, operating systems, and embedded systems. He earned his Ph.D. in Computer Science from the University of Minnesota and worked as a post-doc at INRIA Saclay.