Andrew Gacek is an Industrial Logician at the Rockwell Collins Advanced Technology Center. He earned his PhD in Computer Science from the University of Minnesota and worked as a post-doc at INRIA Saclay. In 2010, he joined Rockwell Collins.

Andrew 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. He has developed various other tools and languages that are in use both inside and outside of Rockwell Collins.

Andrew's broader interests include theorem proving, model checking, language translation, software design, operating systems, and embedded systems.