Andrew Gacek

Publication Activity (10 Years)

Years Active: 2007-2023
Publications (10 Years): 29

Top Topics

Reachability Analysis

Reactive Systems

Access Control Policies

Top Venues

Publications

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, Wen-Mei W. Hwu
CODAG: Characterizing and Optimizing Decompression Algorithms for GPUs. CoRR (2023)
Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi, Vaibhav Sharma, Michael W. Whalen, Raveesh Yadav
Automated Analyses of IOT Event Monitoring Systems. CAV (1) (2023)
Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek, Mats Per Erik Heimdahl
Inductive Validity Cores. IEEE Trans. Software Eng. 47 (2) (2021)
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, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan
Stratified Abstraction of Access Control Policies. CAV (1) (2020)
Malik Bouchet, Byron Cook, Bryant Cutler, Anna Druzkina, Andrew Gacek, Liana Hadarean, Ranjit Jhala, Brad Marshall, Daniel Peebles, Neha Rungta, Cole Schlesinger, Chriss Stephens, Carsten Varming, Andy Warfield
Block public access: trust safety verification of access control policies. ESEC/SIGSOFT FSE (2020)
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
One-Click Formal Methods. IEEE Softw. 36 (6) (2019)
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, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, Blake Whaley
Reachability Analysis for AWS-Based Networks. CAV (2) (2019)
David A. Greve, Andrew Gacek
Trapezoidal Generalization over Linear Constraints. ACL2 (2018)
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
A Formal Approach to Constructing Secure Air Vehicle Software. Computer 51 (11) (2018)
John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Oksana Tkachuk, Carsten Varming
Semantic-based Automated Reasoning for AWS Access Policies using SMT. FMCAD (2018)
Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani
The JKind Model Checker. CAV (2) (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR (2017)
Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani
The JKind Model Checker. CoRR (2017)
Lucas G. Wagner, David A. Greve, Andrew Gacek
SIMPAL: a compositional reasoning framework for imperative programs. SPIN (2017)
Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek
Efficient generation of all minimal inductive validity cores. FMCAD (2017)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Per Erik Heimdahl, Lucas G. Wagner
Proof-based coverage metrics for formal verification. ASE (2017)
Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek
From Design Contracts to Component Requirements Verification. CoRR (2016)
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning About Algebraic Data Types with Abstractions. J. Autom. Reason. 57 (4) (2016)
John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
On Implementing Real-time Specification Patterns Using Observers. CoRR (2016)
Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR (2016)
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning about Algebraic Data Types with Abstractions. CoRR (2016)
Michael W. Whalen, Darren D. Cofer, Andrew Gacek
Requirements and Architectures for Secure Vehicles. IEEE Softw. 33 (4) (2016)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
Efficient Generation of Inductive Validity Cores for Safety Properties. CoRR (2016)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. FormaliSE@ICSE (2016)
Andreas Katis, Michael W. Whalen, Andrew Gacek
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report. CoRR (2016)
Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek
From Design Contracts to Component Requirements Verification. NFM (2016)
John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
On Implementing Real-Time Specification Patterns Using Observers. NFM (2016)
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
Efficient generation of inductive validity cores for safety properties. SIGSOFT FSE (2016)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Machine-Checked Proofs For Realizability Checking Algorithms. CoRR (2015)
Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
Towards Realizability Checking of Contracts using Theories. CoRR (2015)
Andreas Katis, Andrew Gacek, Michael W. Whalen
Machine-Checked Proofs for Realizability Checking Algorithms. VSTTE (2015)
Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer
Towards Realizability Checking of Contracts Using Theories. NFM (2015)
Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen
Resolute: an assurance case language for architecture models. HILT (2014)
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7 (2) (2014)
Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen
Resolute: An Assurance Case Language for Architecture Models. CoRR (2014)
Michael W. Whalen, Andrew Gacek, Darren D. Cofer, Anitha Murugesan, Mats Per Erik Heimdahl, Sanjai Rayadurgam
Your "What" Is My "How": Iteration and Hierarchy in System Design. IEEE Softw. 30 (2) (2013)
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
Reasoning About Higher-Order Relational Specifications CoRR (2013)
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
Reasoning about higher-order relational specifications. PPDP (2013)
Andrew Gacek, Dale Miller, Gopalan Nadathur
A Two-Level Logic Approach to Reasoning About Computations. J. Autom. Reason. 49 (2) (2012)
Andrew Gacek
Abella: A Tutorial. ITP (2012)
Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha
Compositional Verification of Architectural Models. NASA Formal Methods (2012)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Nominal abstraction. Inf. Comput. 209 (1) (2011)
Andrew Gacek
Relating nominal and higher-order abstract syntax specifications. PPDP (2010)
Andrew Gacek
Relating Nominal and Higher-order Abstract Syntax Specifications CoRR (2010)
Andrew Gacek, Dale Miller, Gopalan Nadathur
A two-level logic approach to reasoning about computations CoRR (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Reasoning in Abella about Structural Operational Semantics Specifications. Electron. Notes Theor. Comput. Sci. 228 (2009)
Andrew Gacek
A Framework for Specifying, Prototyping, and Reasoning about Computational Systems CoRR (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Nominal Abstraction CoRR (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Combining generic judgments with recursive definitions CoRR (2008)
Andrew Gacek
System Description: Abella -- A System for Reasoning about Computations CoRR (2008)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Reasoning in Abella about Structural Operational Semantics Specifications CoRR (2008)
Andrew Gacek
The Abella Interactive Theorem Prover (System Description). IJCAR (2008)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Combining Generic Judgments with Recursive Definitions. LICS (2008)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr system for model checking over syntactic expressions CoRR (2007)
Andrew Gacek, Gopalan Nadathur
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi CoRR (2007)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr System for Model Checking over Syntactic Expressions. CADE (2007)
Andrew Gacek
The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi CoRR (2007)