default search action
Andrew Gacek
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [c26]Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi, Vaibhav Sharma
, Michael W. Whalen
Automated Analyses of IOT Event Monitoring Systems. CAV (1) 2023: 27-39 - [i23]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 abs/2307.03760 (2023) - 2021
- [j9]Elaheh Ghassabani
Inductive Validity Cores. IEEE Trans. Software Eng. 47(2): 279-299 (2021) - 2020
- [c25]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: 165-176 - [c24]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: 281-291
2010 – 2019
- 2019
- [j8]John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf
One-Click Formal Methods. IEEE Softw. 36(6): 61-65 (2019) - [c23]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: 231-241 - 2018
- [j7]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): 14-23 (2018) - [c22]Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani:
The JKind Model Checker. CAV (2) 2018: 20-27 - [c21]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: 1-9 - [c20]Andreas Katis
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) 2018: 176-193 - [c19]David A. Greve, Andrew Gacek:
Trapezoidal Generalization over Linear Constraints. ACL2 2018: 30-46 - 2017
- [c18]Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek:
Efficient generation of all minimal inductive validity cores. FMCAD 2017: 31-38 - [c17]Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats Per Erik Heimdahl, Lucas G. Wagner:
Proof-based coverage metrics for formal verification. ASE 2017: 194-199 - [c16]Lucas G. Wagner, David A. Greve, Andrew Gacek:
SIMPAL: a compositional reasoning framework for imperative programs. SPIN 2017: 90-93 - [i22]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 abs/1709.04986 (2017) - [i21]Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner, Elaheh Ghassabani:
The JKind Model Checker. CoRR abs/1712.01222 (2017) - 2016
- [j6]Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen:
Reasoning About Algebraic Data Types with Abstractions. J. Autom. Reason. 57(4): 281-318 (2016) - [j5]Michael W. Whalen, Darren D. Cofer, Andrew Gacek:
Requirements and Architectures for Secure Vehicles. IEEE Softw. 33(4): 22-25 (2016) - [c15]Andreas Katis
Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. FormaliSE@ICSE 2016: 36-41 - [c14]John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp
On Implementing Real-Time Specification Patterns Using Observers. NFM 2016: 19-33 - [c13]Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek:
From Design Contracts to Component Requirements Verification. NFM 2016: 373-387 - [c12]Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen:
Efficient generation of inductive validity cores for safety properties. SIGSOFT FSE 2016: 314-325 - [i20]Andreas Katis, Michael W. Whalen, Andrew Gacek:
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report. CoRR abs/1602.00148 (2016) - [i19]Jing Liu, John D. Backes, Darren D. Cofer, Andrew Gacek:
From Design Contracts to Component Requirements Verification. CoRR abs/1603.02130 (2016) - [i18]Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen:
Efficient Generation of Inductive Validity Cores for Safety Properties. CoRR abs/1603.04276 (2016) - [i17]Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen:
Reasoning about Algebraic Data Types with Abstractions. CoRR abs/1603.08769 (2016) - [i16]John D. Backes, Michael W. Whalen, Andrew Gacek, John Komp:
On Implementing Real-time Specification Patterns Using Observers. CoRR abs/1604.08155 (2016) - [i15]Andreas Katis, Grigory Fedyukovich
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR abs/1610.05867 (2016) - 2015
- [c11]Andrew Gacek, Andreas Katis
Towards Realizability Checking of Contracts Using Theories. NFM 2015: 173-187 - [c10]Andreas Katis
Machine-Checked Proofs for Realizability Checking Algorithms. VSTTE 2015: 110-123 - [i14]Andreas Katis, Andrew Gacek, Michael W. Whalen:
Machine-Checked Proofs For Realizability Checking Algorithms. CoRR abs/1502.01292 (2015) - [i13]Andrew Gacek, Andreas Katis, Michael W. Whalen, John Backes, Darren D. Cofer:
Towards Realizability Checking of Contracts using Theories. CoRR abs/1502.03005 (2015) - 2014
- [j4]David Baelde
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7(2): 1-89 (2014) - [c9]Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen:
Resolute: an assurance case language for architecture models. HILT 2014: 19-28 - [i12]Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen:
Resolute: An Assurance Case Language for Architecture Models. CoRR abs/1409.4629 (2014) - 2013
- [j3]Michael W. Whalen, Andrew Gacek, Darren D. Cofer, Anitha Murugesan
Your "What" Is My "How": Iteration and Hierarchy in System Design. IEEE Softw. 30(2): 54-60 (2013) - [c8]Yuting Wang
Reasoning about higher-order relational specifications. PPDP 2013: 157-168 - [i11]Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur:
Reasoning About Higher-Order Relational Specifications. CoRR abs/1302.2584 (2013) - 2012
- [j2]Andrew Gacek, Dale Miller
A Two-Level Logic Approach to Reasoning About Computations. J. Autom. Reason. 49(2): 241-273 (2012) - [c7]Andrew Gacek:
Abella: A Tutorial. ITP 2012: 49-50 - [c6]Darren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha:
Compositional Verification of Architectural Models. NASA Formal Methods 2012: 126-140 - 2011
- [j1]Andrew Gacek, Dale Miller
Nominal abstraction. Inf. Comput. 209(1): 48-73 (2011) - 2010
- [c5]Andrew Gacek:
Relating nominal and higher-order abstract syntax specifications. PPDP 2010: 177-186 - [i10]Andrew Gacek:
Relating Nominal and Higher-order Abstract Syntax Specifications. CoRR abs/1003.5447 (2010)
2000 – 2009
- 2009
- [i9]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Nominal Abstraction. CoRR abs/0908.1390 (2009) - [i8]Andrew Gacek:
A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. CoRR abs/0910.0747 (2009) - [i7]Andrew Gacek, Dale Miller, Gopalan Nadathur:
A two-level logic approach to reasoning about computations. CoRR abs/0911.2993 (2009) - 2008
- [c4]Andrew Gacek:
The Abella Interactive Theorem Prover (System Description). IJCAR 2008: 154-161 - [c3]Andrew Gacek, Dale Miller
Combining Generic Judgments with Recursive Definitions. LICS 2008: 33-44 - [c2]Andrew Gacek, Dale Miller
Reasoning in Abella about Structural Operational Semantics Specifications. LFMTP@LICS 2008: 85-100 - [i6]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Combining generic judgments with recursive definitions. CoRR abs/0802.0865 (2008) - [i5]Andrew Gacek:
System Description: Abella -- A System for Reasoning about Computations. CoRR abs/0803.2305 (2008) - [i4]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Reasoning in Abella about Structural Operational Semantics Specifications. CoRR abs/0804.3914 (2008) - 2007
- [c1]David Baelde, Andrew Gacek, Dale Miller
The Bedwyr System for Model Checking over Syntactic Expressions. CADE 2007: 391-397 - [i3]Andrew Gacek:
The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi. CoRR abs/cs/0702027 (2007) - [i2]David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu:
The Bedwyr system for model checking over syntactic expressions. CoRR abs/cs/0702116 (2007) - [i1]Andrew Gacek, Gopalan Nadathur:
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi. CoRR abs/cs/0702152 (2007)
Coauthor Index
aka: John Backes
aka: Mike Whalen
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: