Andrew Gacek

Industrial Logician

Andrew Gacek is an Industrial Logician at the Rockwell Collins Advanced Technology Center.

Andrew earned his PhD in Computer Science from the University of Minnesota in 2009 and continued his studies as a post-doc INRIA Saclay as part of Parsifal group. In 2010, Andrew joined Rockwell Collins. He is currently working as part of the air vehicle team in DARPA's High Assurance Cyber Military Systems project (HACMS), focusing high-level structural and behavioral properties for unmanned air vehicles.

Andrew has a strong interest in developing tools for the application of formal methods. As part of his PhD thesis, Andrew created the Abella theorem prover, an interactive theorem prover based on lambda-tree syntax. At Rockwell Collins, Andrew developed JKind, an infinite-state model checker for safety properties. JKind is used for both various internal and external projects at Rockwell Collins. Most recently, Andrew developed the Resolute language and tool for architecturally-structured assurance cases.

His interests include theorem proving, model checking, language translation, and software design.