The Bedwyr System for Model Checking over Syntactic Expressions. - David Baelde; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu (CADE, 2007)

The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi - Andrew Gacek (CoRR, 2007)

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi - Andrew Gacek; Gopalan Nadathur (CoRR, 2007)

The Abella Interactive Theorem Prover (System Description). - Andrew Gacek (IJCAR, 2008)

Combining Generic Judgments with Recursive Definitions. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LICS, 2008)

System Description: Abella – A System for Reasoning about Computations - Andrew Gacek (CoRR, 2008)

Reasoning in Abella about Structural Operational Semantics Specifications. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LFMTP@LICS, 2008)

A Framework for Specifying, Prototyping, and Reasoning about Computational Systems - Andrew Gacek (CoRR, 2009)

Relating nominal and higher-order abstract syntax specifications. - Andrew Gacek (PPDP, 2010)

Nominal abstraction. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (Inf. Comput., 2011)

Abella: A Tutorial. - Andrew Gacek (ITP, 2012)

Compositional Verification of Architectural Models. - Darren D. Cofer; Andrew Gacek; Steven P. Miller; Michael W. Whalen; Brian LaValley; Lui Sha (NASA Formal Methods, 2012)

A Two-Level Logic Approach to Reasoning About Computations. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (J. Autom. Reason., 2012)

Reasoning about higher-order relational specifications. - Yuting Wang 001; Kaustuv Chaudhuri; Andrew Gacek; Gopalan Nadathur (PPDP, 2013)

Your "What" Is My "How": Iteration and Hierarchy in System Design. - Michael W. Whalen; Andrew Gacek; Darren D. Cofer; Anitha Murugesan; Mats Per Erik Heimdahl; Sanjai Rayadurgam (IEEE Softw., 2013)

Resolute: an assurance case language for architecture models. - Andrew Gacek; John Backes; Darren D. Cofer; Konrad Slind; Mike Whalen (HILT, 2014)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

Towards Realizability Checking of Contracts Using Theories. - Andrew Gacek; Andreas Katis; Michael W. Whalen; John Backes; Darren D. Cofer (NFM, 2015)

Machine-Checked Proofs for Realizability Checking Algorithms. - Andreas Katis; Andrew Gacek; Michael W. Whalen (VSTTE, 2015)

Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. - Andreas Katis; Andrew Gacek; Michael W. Whalen (FormaliSE@ICSE, 2016)

On Implementing Real-Time Specification Patterns Using Observers. - John D. Backes; Michael W. Whalen; Andrew Gacek; John Komp (NFM, 2016)

From Design Contracts to Component Requirements Verification. - Jing Liu; John D. Backes; Darren D. Cofer; Andrew Gacek (NFM, 2016)

Efficient generation of inductive validity cores for safety properties. - Elaheh Ghassabani; Andrew Gacek; Michael W. Whalen (SIGSOFT FSE, 2016)

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. - Andreas Katis; Grigory Fedyukovich; Andrew Gacek; John D. Backes; Arie Gurfinkel; Michael W. Whalen (CoRR, 2016)

Reasoning About Algebraic Data Types with Abstractions. - Tuan-Hung Pham; Andrew Gacek; Michael W. Whalen (J. Autom. Reason., 2016)

Requirements and Architectures for Secure Vehicles. - Michael W. Whalen; Darren D. Cofer; Andrew Gacek (IEEE Softw., 2016)

Efficient generation of all minimal inductive validity cores. - Elaheh Ghassabani; Michael W. Whalen; Andrew Gacek (FMCAD, 2017)

Proof-based coverage metrics for formal verification. - Elaheh Ghassabani; Andrew Gacek; Michael W. Whalen; Mats Per Erik Heimdahl; Lucas G. Wagner (ASE, 2017)

SIMPAL: a compositional reasoning framework for imperative programs. - Lucas G. Wagner; David A. Greve; Andrew Gacek (SPIN, 2017)

The JKind Model Checker. - Andrew Gacek; John Backes; Mike Whalen; Lucas G. Wagner; Elaheh Ghassabani (CAV (2), 2018)

Semantic-based Automated Reasoning for AWS Access Policies using SMT. - John Backes; Pauline Bolignano; Byron Cook; Catherine Dodge; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Oksana Tkachuk; Carsten Varming (FMCAD, 2018)

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. - Andreas Katis; Grigory Fedyukovich; Huajun Guo; Andrew Gacek; John Backes; Arie Gurfinkel; Michael W. Whalen (TACAS (2), 2018)

A Formal Approach to Constructing Secure Air Vehicle Software. - Darren D. Cofer; Andrew Gacek; John Backes; Michael W. Whalen; Lee Pike; Adam Foltzer; Michal Podhradsky; Gerwin Klein; Ihor Kuz; June Andronick; Gernot Heiser; Douglas Stuart (Computer, 2018)

Trapezoidal Generalization over Linear Constraints. - David A. Greve; Andrew Gacek (ACL2, 2018)

Reachability Analysis for AWS-Based Networks. - John Backes; Sam Bayless; Byron Cook; Catherine Dodge; Andrew Gacek; Alan J. Hu; Temesghen Kahsai; Bill Kocik; Evgenii Kotelnikov; Jure Kukovec; Sean McLaughlin; Jason Reed 004; et al. (CAV (2), 2019)

One-Click Formal Methods. - John Backes; Pauline Bolignano; Byron Cook; Andrew Gacek; Kasper Søe Luckow; Neha Rungta; Martin Schäf; Cole Schlesinger; Rima Tanash; Carsten Varming; Michael W. Whalen (IEEE Softw., 2019)

Stratified Abstraction of Access Control Policies. - John Backes; Ulises Berrueco; Tyler Bray; Daniel Brim; Byron Cook; Andrew Gacek; Ranjit Jhala; Kasper Søe Luckow; Sean McLaughlin; Madhav Menon; Daniel Peebles; Ujjwal Pugalia; et al. (CAV (1), 2020)

Block public access: trust safety verification of access control policies. - Malik Bouchet; Byron Cook; Bryant Cutler; Anna Druzkina; Andrew Gacek; Liana Hadarean; Ranjit Jhala; Brad Marshall; Daniel Peebles; Neha Rungta; Cole Schlesinger; Chriss Stephens; et al. (ESEC/SIGSOFT FSE, 2020)

Inductive Validity Cores. - Elaheh Ghassabani; Michael W. Whalen; Andrew Gacek; Mats Per Erik Heimdahl (IEEE Trans. Software Eng., 2021)

Automated Analyses of IOT Event Monitoring Systems. - Andrew Apicelli; Sam Bayless; Ankush Das; Andrew Gacek; Dhiva Jaganathan; Saswat Padhi; Vaibhav Sharma 001; Michael W. Whalen; Raveesh Yadav (CAV (1), 2023)

CODAG: Characterizing and Optimizing Decompression Algorithms for GPUs. - Jeongmin Brian Park; Zaid Qureshi; Vikram S. Mailthody; Andrew Gacek; Shunfan Shao; Mohammad Almasri; Isaac Gelado; Jinjun Xiong; Chris J. Newburn; I-Hsin Chung; Michael Garland; Nikolay Sakharnykh; et al. (CoRR, 2023)

Projective Model Counting for IP Addresses in Access Control Policies. - Loris D'Antoni; Andrew Gacek; Amit Goel; Dejan Jovanovic; Rami Gökhan Kici; Daniel Peebles; Neha Rungta; Yasmine Sharoda; Chungha Sung (FMCAD, 2024)