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.
- Video: HACMS – Cybersecurity for Military and Commercial Aircraft
- SIMPAL: A Compositional Reasoning Framework for Imperative Programs
- Video: High-Assurance Cyber Military Systems (HACMS)
- From Design Contracts to Component Requirements Verification
- Requirements and Architectures for Secure Vehicles
- On Implementing Real-time Specification Patterns Using Observers
- Towards Realizability Checking of Contracts using Theories