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 is currently working as part of the air vehicle team in DARPA's High Assurance Cyber Military Systems program. He is also working on the NASA funded project: Compositional Verification of Flight Critical Systems. His interests include SMT-Solving, Model Checking, and Logic Synthesis.
- 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.