Andrew Gacek

According to our database, Andrew Gacek authored at least 41 papers between 2007 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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, Wen-Mei W. Hwu

CoRR, 2023

Automated Analyses of IOT Event Monitoring Systems.

Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi, Vaibhav Sharma, Michael W. Whalen, Raveesh Yadav

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2021

Inductive Validity Cores.

Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek, Mats Per Erik Heimdahl

IEEE Trans. Software Eng., 2021

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, Carsten Varming, Andy Warfield

Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

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, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

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

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, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, Blake Whaley

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Trapezoidal Generalization over Linear Constraints.

David A. Greve, Andrew Gacek

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 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

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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

The JKind Model Checker.

Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

SIMPAL: a compositional reasoning framework for imperative programs.

Lucas G. Wagner, David A. Greve, Andrew Gacek

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Proof-based coverage metrics for formal verification.

Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Per Erik Heimdahl, Lucas G. Wagner

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Efficient generation of all minimal inductive validity cores.

Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

Requirements and Architectures for Secure Vehicles.

Michael W. Whalen, Darren D. Cofer, Andrew Gacek

IEEE Softw., 2016

Reasoning About Algebraic Data Types with Abstractions.

Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen

J. Autom. Reason., 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

Efficient generation of inductive validity cores for safety properties.

Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

From Design Contracts to Component Requirements Verification.

Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

On Implementing Real-Time Specification Patterns Using Observers.

John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report.

Andreas Katis, Andrew Gacek, Michael W. Whalen

Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, 2016

2015

Machine-Checked Proofs for Realizability Checking Algorithms.

Andreas Katis, Andrew Gacek, Michael W. Whalen

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Towards Realizability Checking of Contracts Using Theories.

Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

2014

Abella: A System for Reasoning about Relational Specifications.

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang

J. Formaliz. Reason., 2014

Resolute: an assurance case language for architecture models.

Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen

Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

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

Reasoning about higher-order relational specifications.

Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

2012

A Two-Level Logic Approach to Reasoning About Computations.

Andrew Gacek, Dale Miller, Gopalan Nadathur

J. Autom. Reason., 2012

Compositional Verification of Architectural Models.

Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha

Proceedings of the NASA Formal Methods, 2012

Abella: A Tutorial.

Andrew Gacek

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Nominal abstraction.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Inf. Comput., 2011

2010

Relating nominal and higher-order abstract syntax specifications.

Andrew Gacek

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

2009

A Framework for Specifying, Prototyping, and Reasoning about Computational Systems

Andrew Gacek

CoRR, 2009

2008

Reasoning in Abella about Structural Operational Semantics Specifications.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

System Description: Abella -- A System for Reasoning about Computations

Andrew Gacek

CoRR, 2008

Combining Generic Judgments with Recursive Definitions.

Andrew Gacek, Dale Miller, Gopalan Nadathur

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

The Abella Interactive Theorem Prover (System Description).

Andrew Gacek

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi

Andrew Gacek, Gopalan Nadathur

CoRR, 2007

The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi

Andrew Gacek

CoRR, 2007

The Bedwyr System for Model Checking over Syntactic Expressions.

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu

Proceedings of the Automated Deduction, 2007