| Ghost talk: Mitigating EMI signal injection attacks against analog sensors DF Kune, J Backes, SS Clark, D Kramer, M Reynolds, K Fu, Y Kim, W Xu 2013 IEEE Symposium on Security and Privacy, 145-159, 2013 | 512 | 2013 |
| 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 | 147 | 2018 |
| 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 | 75 | 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 | 73 | 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 | 69 | 2019 |
| Regression verification using impact summaries J Backes, S Person, N Rungta, O Tkachuk Model Checking Software: 20th International Symposium, SPIN 2013, Stony …, 2013 | 62 | 2013 |
| Requirements analysis of a quad-redundant flight control system J Backes, D Cofer, S Miller, MW Whalen NASA Formal Methods Symposium, 82-96, 2015 | 45 | 2015 |
| 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 | 41 | 2015 |
| 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 | 37 | 2018 |
| One-click formal methods J Backes, P Bolignano, B Cook, A Gacek, KS Luckow, N Rungta, ... IEEE Software 36 (6), 61-65, 2019 | 36 | 2019 |
| 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 | 30 | 2018 |
| The analysis of cyclic circuits with Boolean satisfiability J Backes, B Fett, MD Riedel 2008 IEEE/ACM International Conference on Computer-Aided Design, 143-148, 2008 | 25 | 2008 |
| The synthesis of stochastic circuits for nanoscale computation W Qian, J Backes, MD Riedel International Journal of Nanotechnology and Molecular Computation (IJNMC) 1 …, 2009 | 20 | 2009 |
| Secure mathematically-assured composition of control models D Cofer, J Backes, A Gacek, D DaCosta, M Whalen, I Kuz, G Klein, ... Air Force Research Laboratory Information Directorate, 2017 | 13 | 2017 |
| From design contracts to component requirements verification J Liu, JD Backes, D Cofer, A Gacek NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN …, 2016 | 13 | 2016 |
| Reduction of interpolants for logic synthesis JD Backes, MD Riedel 2010 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 602-609, 2010 | 13 | 2010 |
| Stratified abstraction of access control policies J Backes, U Berrueco, T Bray, D Brim, B Cook, A Gacek, R Jhala, ... Computer Aided Verification: 32nd International Conference, CAV 2020, Los …, 2020 | 12 | 2020 |
| The synthesis of cyclic dependencies with Boolean satisfiability JD Backes, MD Riedel ACM Transactions on Design Automation of Electronic Systems (TODAES) 17 (4 …, 2012 | 9 | 2012 |
| Synthesis from assume-guarantee contracts using skolemized proofs of realizability A Katis, G Fedyukovich, A Gacek, J Backes, A Gurfinkel, MW Whalen arXiv preprint arXiv:1610.05867, 2016 | 8 | 2016 |
| Using cubes of non-state variables with property directed reachability JD Backes, MD Riedel 2013 Design, Automation & Test in Europe Conference & Exhibition (DATE), 807-810, 2013 | 6 | 2013 |
