Andrew Gacek

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