John Backes is a Senior Research Scientist at the Rockwell Collins Advanced Technology Center. He earned his PhD from the Department of Electrical and Computer Engineering at the University of Minnesota. He is the principle developer of AGREE, a compositional verification tool for AADL models. He was a member of the air vehicle team in DARPA's High Assurance Cyber Military Systems program. He has also been a performer on projects funded by NASA, AFRL, and the Army. He is currently working on verification of AFRL's UxAS as part of the Summer of Innovation. His research interests include SMT-Solving, Model Checking, Formalization of Requirements, Verification of Software for Embedded Systems, and Logic Synthesis.
Most birds lay their eggs in nests, and the nestlings remain in the nest for days or weeks. Not loons! It would be incorrect to call loon chicks "nestlings" for more than a few hours. Once they leave the nest, they're out of there for good!
Publications
- The Assume Guarantee Reasoning Environment with Application to an Unmanned Helicopter. J. Backes, D. Cofer, I. Amundson. Technical Report. 2021.
- A Formal Approach to Constructing Secure Air Vehicle Software. D. Cofer, A. Gacek, J. Backes, M. Whalen, L. Pike, A. Foltzer, M. Podhradsky, G. Klein, I. Kuz, J. Andronick, G. Heiser, D. Stuart. IEEE Computer Magazine, November 2018.
- The JKind Model Checker. A. Gacek, J. Backes, M. Whalen, L. Wagner, E. Ghassabani. Computer Aided Verification 2018.
- Secure Mathematically-Assured Composition of Control Models. D. Cofer, J. Backes, A. Gacek, D. DaCosta, M. Whalen, I. Kuz, G. Klein, G. Heiser, L. Pike, A. Foltzer, M. Podhradsky, D. Stuart, J. Grahan, B. Wilson. HACMS Final Report, October 2017.
- Trapezoidal Generalization of Lustre with Uninterpreted Functions. D. Greve, J. Backes. Technical Report. 2017.
- From Design Contracts to Component Requirements Verification. J. Liu, J. Backes, D. Cofer, A. Gacek. NASA Formal Methods Symposium, June 2016.
- On Implementing Real-time Specification Patterns Using Observers. J. Backes, M. Whalen, A. Gacek, J. Komp. NASA Formal Methods Symposium, June 2016.
- Requirements Analysis of a Quad-Redundant Flight Control System. J. Backes, D. Cofer, S. Miller, M. Whalen. NASA Formal Methods Symposium, 2015.
- Towards realizability checking of contracts using theories. A. Gacek, A. Katis, M. Whalen, J. Backes, D. Cofer. NASA Formal Methods, 2015.
- Resolute: an assurance case language for architecture models. A. Gacek, J. Backes, D. Cofer, K. Slind, M. Whalen. HILT 2014.
- Ghost Talk: Mitigating EMI Signal Injection Attacks against Analog Sensors. D. Kune, J. Backes, S. Clark, D. Kramer, M. Reynolds, K. Fu, Y. Kim, W. Xu. Proceedings of IEEE Symposium on Security and Privacy, 2013.
- Regression Verification Using Impact Summaries. J. Backes, S. Person, N. Rungta, O. Tkachuk. In proceedings of the 20th International SPIN Symposium on Model Checking of Software, 2013.
- Algorithms and Data Structures for Logic Synthesis and Verfication Using Boolean Satisfiability. J. Backes. Ph.D. Thesis, University of Minnesota, March 2013.
- Using Cubes of Non-state Variables With Property Directed Reachability. J. Backes, M. Riedel. Proceedings of Design Automation and Test in Europe, Grenoble, France. 2013.
- The Synthesis of Cyclic Dependencies with Boolean Satisfiability. J. Backes, M. Riedel. Transactions on Design Automation of Electronic Systems, 2012.
- The Analysis and Mapping of Cyclic Circuits with Boolean Satisfiability. J. Backes, B. Fett, M. Riedel. Technical Report. 2011.
- Resolution Proofs as a Data Structure for Logic Synthesis. J. Backes, M. Riedel. Proceedings of the International Workshop on Logic Synthesis, La Jolla, CA. 2011.
- The Synthesis of Stochastic Circuits for Nanoscale Computation. W. Qian, J. Backes, M. Riedel. International Journal of Nanotechnology and Molecular Computation, pp. 39-57, 2010.
- Reduction of Interpolants for Logic Synthesis. J. Backes, M. Riedel. Proceedings of the International Conference on Computer-Aided Design, San Jose, CA. 2010.
- The Synthesis of Cyclic Dependencies with Craig Interpolation. J. Backes, M. Riedel. Proceedings of the International Workshop on Logic Synthesis, Berkeley, CA. 2009.
- The Analysis of Cyclic Circuits with Boolean Satisfiability. J. Backes, B. Fett, M. Riedel. Proceedings of the International Conference on Computer-Aided Design, San Jose, CA. 2008.