| 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 | 184 | 2018 |
| 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 | 172 | 2012 |
| The Abella interactive theorem prover (system description) A Gacek Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney …, 2008 | 128 | 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 | 119 | 2014 |
| 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 | 93 | 2012 |
| 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 | 93 | 2007 |
| 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 | 86 | 2014 |
| 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 | 82 | 2019 |
| The JKind Model Checker A Gacek, J Backes, M Whalen, L Wagner, E Ghassabani Computer Aided Verification: 30th International Conference, CAV 2018, Held …, 2018 | 79 | 2018 |
| 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 | 69 | 2021 |
| A two-level logic approach to reasoning about computations A Gacek, D Miller, G Nadathur Journal of Automated Reasoning 49 (2), 241-273, 2012 | 68 | 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 | 67 | 2008 |
| Nominal abstraction A Gacek, D Miller, G Nadathur Information and Computation 209 (1), 48-73, 2011 | 66 | 2011 |
| 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 | 44 | 2015 |
| One-click formal methods J Backes, P Bolignano, B Cook, A Gacek, KS Luckow, N Rungta, ... IEEE Software 36 (6), 61-65, 2019 | 43 | 2019 |
| A framework for specifying, prototyping, and reasoning about computational systems AJ Gacek University of Minnesota, 2009 | 43 | 2009 |
| 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 | 39 | 2018 |
| 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 | 38 | 2018 |
| 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 | 38 | 2016 |
| Reasoning in Abella about structural operational semantics specifications A Gacek, D Miller, G Nadathur Electronic Notes in Theoretical Computer Science 228, 85-100, 2009 | 33 | 2009 |
Michael W WhalenAmazon, Inc. and the University of MinnesotaVerified email at cs.umn.edu
