Andrew Gacek
Andrew Gacek
Amazon Web Service
Verified email at
Cited by
Cited by
Compositional verification of architectural models
D Cofer, A Gacek, S Miller, MW Whalen, B LaValley, L Sha
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA …, 2012
Semantic-based automated reasoning for AWS access policies using SMT
J Backes, P Bolignano, B Cook, C Dodge, A Gacek, K Luckow, N Rungta, ...
2018 Formal Methods in Computer Aided Design (FMCAD), 1-9, 2018
The Abella interactive theorem prover (system description)
A Gacek
Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney …, 2008
Abella: A system for reasoning about relational specifications
D Baelde, K Chaudhuri, A Gacek, D Miller, G Nadathur, A Tiu, Y Wang
Journal of formalized reasoning 7 (2), 1-89, 2014
The Bedwyr system for model checking over syntactic expressions
D Baelde, A Gacek, D Miller, G Nadathur, A Tiu
Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007
Your" what" is my" how": Iteration and hierarchy in system design
MW Whalen, A Gacek, D Cofer, A Murugesan, MPE Heimdahl, ...
IEEE software 30 (2), 54-60, 2012
Resolute: an assurance case language for architecture models
A Gacek, J Backes, D Cofer, K Slind, M Whalen
ACM SIGAda Ada Letters 34 (3), 19-28, 2014
The JKind Model Checker
A Gacek, J Backes, M Whalen, L Wagner, E Ghassabani
Computer Aided Verification: 30th International Conference, CAV 2018, Held …, 2018
Reachability analysis for AWS-based networks
J Backes, S Bayless, B Cook, C Dodge, A Gacek, AJ Hu, T Kahsai, ...
Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019
A two-level logic approach to reasoning about computations
A Gacek, D Miller, G Nadathur
Journal of Automated Reasoning 49 (2), 241-273, 2012
Combining generic judgments with recursive definitions
A Gacek, D Miller, G Nadathur
2008 23rd Annual IEEE Symposium on Logic in Computer Science, 33-44, 2008
Nominal abstraction
A Gacek, D Miller, G Nadathur
Information and Computation 209 (1), 48-73, 2011
Constraint solver execution service and infrastructure therefor
N Rungta, TK Azene, PV Bolignano, KS Luckow, S McLaughlin, C Dodge, ...
US Patent 10,977,111, 2021
Towards realizability checking of contracts using theories
A Gacek, A Katis, MW Whalen, J Backes, D Cofer
NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA …, 2015
A framework for specifying, prototyping, and reasoning about computational systems
AJ Gacek
University of Minnesota, 2009
Efficient generation of inductive validity cores for safety properties
E Ghassabani, A Gacek, MW Whalen
Proceedings of the 2016 24th ACM SIGSOFT International Symposium on …, 2016
One-click formal methods
J Backes, P Bolignano, B Cook, A Gacek, KS Luckow, N Rungta, ...
IEEE Software 36 (6), 61-65, 2019
A formal approach to constructing secure air vehicle software
D Cofer, A Gacek, J Backes, MW Whalen, L Pike, A Foltzer, M Podhradsky, ...
Computer 51 (11), 14-23, 2018
Validity-guided synthesis of reactive systems from assume-guarantee contracts
A Katis, G Fedyukovich, H Guo, A Gacek, J Backes, A Gurfinkel, ...
Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018
Reasoning in Abella about structural operational semantics specifications
A Gacek, D Miller, G Nadathur
Electronic Notes in Theoretical Computer Science 228, 85-100, 2009
The system can't perform the operation now. Try again later.
Articles 1–20