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's expertise is integrating new and exciting research topics into tools which put formal methods in the hands of real users. Andrew is the author of JKind, an infinite-state model checker for safety properties. He advocates for the use of JKind which now underlies tools such as AGREE, SpeAR, and SIMPAL. In addition, JKind serves as a research platform to investigate topics such as realizability and inductive validity cores. Andrew also created the Abella theorem prover and the Resolute assurance case tool.
Andrew's broader interests include theorem proving, model checking, language translation, software design, operating systems, and embedded systems.
