- Run-Time Assurance for Learning-Based Aircraft Taxiing. D. Cofer, I. Amundson, R. Sattigeri, A. Passi, C. Boggs, E. Smith, L. Gilham, T. Byun, S. Rayadurgam. Digital Avionics Systems Conference, October 2020.
- Run-Time Assurance for Learning-Enabled Systems. D. Cofer, I. Amundson, R. Sattigeri, A. Passi, C. Boggs, E. Smith, L. Gilham, T. Byun, S. Rayadurgam. NASA Formal Methods Symposium, May 2020.
- Safety Annex for the Architecture Analysis and Design Language. D. Stewart, J. Liu, D. Cofer, M. Heimdahl, M. Whalen, M. Peterson. Embedded Real Time Systems Conference, January 2020.
- Trapezoidal Generalization over Linear Constraints. D. Greve, A. Gacek. 15th International Workshop on the ACL2 Theorem Prover and Its Applications, November 2018.
- 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.
- FuzzM: A Model-Based Approach to Grey-Box Fuzzing. R. Coppa, G. Foudree, D. Greve. Technical Report. 2018.
- Proof-Based Coverage Metrics for Formal Verification. E. Ghassabani, M. Whalen, M. Heimdahl, A. Gacek, L. Wagner. Automated Software Engineering, October 2017.
- 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.
- Efficient Generation of All Minimal Inductive Validity Cores. E. Ghassabani, M. Whalen, A. Gacek. Formal Methods in Computer-Aided Design, October 2017.
- Architectural Modeling and Analysis for Safety Engineering. D. Stewart, M. Whalen, D. Cofer, M. Heimdahl. International Symposium on Model-Based Safety and Assessment, September 2017.
- Trapezoidal Generalization of Lustre with Uninterpreted Functions. D. Greve, J. Backes. Technical Report. 2017.
- SIMPAL: A Compositional Reasoning Framework for Imperative Programs. L. Wagner, D. Greve, A. Gacek. International SPIN Symposium on Model Checking of Software, July 2017.
- Generalization Correctness. D. Greve. 14th International Workshop on the ACL2 Theorem Prover and Its Applications, May 2017.
- SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements. A. Fifarek, L. Wagner, E. Hoffman, B. Rodes, M. Aiello, J. Davis. NASA Formal Methods Symposium, May 2017.
- Qualification of a Model Checker for Avionics Software Verification. L. Wagner, A. Mebsout, C. Tinelli, D. Cofer, K. Slind. NASA Formal Methods Symposium, May 2017.
- Formal Methods Tool Qualification. L. Wagner, D. Cofer, K. Slind, C. Tinelli, A. Mebsout. NASA Contractor Report NASA/CR-2017-219371, 2017.
- Efficient Generation of Inductive Validity Cores for Safety Properties. E. Ghassabani, A. Gacek, M. Whalen. Foundations of Software Engineering, November 2016.
- Requirements and Architectures for Secure Vehicles. M. Whalen, D. Cofer, A. Gacek. IEEE Software 33(4):22-25, June 2016, doi:10.1109/MS.2016.94.
- 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.
- Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. A. Katis, M. Whalen, A. Gacek. FormaliSE 2016: FME Workshop on Formal Methods in Software Engineering, Austin, TX, USA, May 15, 2016.
- Reasoning about Algebraic Data Types with Abstractions. T. Pham, A. Gacek, M. Whalen. Journal of Automated Reasoning (2016). doi:10.1007/s10817-016-9368-2.
- Taming the Complexity Beast. D. Cofer. International Test and Evaluation Association (ITEA) Journal, December 2015.
- Formal Requirements of a Simple Turbofan Using the SpeAR Framework. A. Fifarek, L. Wagner. International Society for Air Breathing Engines (ISABE), October 2015.
- You Keep Using That Word. D. Cofer. ACM Special Interest Group on Logic and Computation (SIGLOG) Newsletter, October 2015.
- Qualification of Formal Methods Tools. D. Cofer, G. Klein, K. Slind, V. Wiels. Dagstuhl Seminar 15182.
- Machine-checked proofs for realizability checking algorithms. A. Katis, A. Gacek, M. Whalen. 7th Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2015), San Fransisco, CA, USA, July 18-19, 2015.
- Formal Verification of Quasi-Synchronous Systems. S. Miller, S. Bhattacharyya, C. Tinelli, S. Smolka, C. Sticksel, B. Meng, J. Yang. Final Technical Report delivered Air Force Research Laboratory, July 2015.
- Certification Considerations for Adaptive Systems. S. Bhattacharyya, D. Cofer, D. Musliner, J. Mueller, E. Engstrom. International Conference on Unmanned Aircraft Systems, 2015.
- Enhancing Autonomy with Trusted Cognitive Modeling. S. Bhattacharyya, J. Davis, T. Vogl, M. Fix, A. McLean, M. Matessa, L. Smith-Velazquez. AUVSI Unmanned Systems, May 2015.
- 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.
- 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. Vol 7, No 2, pp. 1-89.
- Resolute: an assurance case language for architecture models. A. Gacek, J. Backes, D. Cofer, K. Slind, M. Whalen. HILT 2014.
- DO-333 Certification Case Studies. D. Cofer, S. Miller. NASA Formal Methods Symposium, 2014.
- Formal Methods Case Studies for DO-333. D. Cofer, S. Miller. NASA Contractor Report NASA/CR-2014-218244, 2014.
- Creating Formally Verified Components for Layered Assurance with an LLVM to ACL2 Translator. D. Hardin, J. McClurg, J. Davis. 7th Layered Assurance Workshop, December 2013.
- Study on the Barriers to the Industrial Adoption of Formal Methods. J. Davis, M. Clark, D. Cofer, A. Fifarek, J. Hinchman, J. Hoffman, B. Hulbert, S. Miller, L. Wagner. FMICS 2013.
- Reasoning about higher-order relational specifications. Y. Wang, K. Chaudhuri, A. Gacek, G. Nadathur. The 15th Symposium on Principles and Practice of Declarative Programming (PPDP), 2013.
- Your "what" is my "how": iteration and hierarchy in system design. M. Whalen, A. Gacek, D. Cofer, A. Murugesan, M. Heimdahl, S. Rayadurgam. IEEE Software, vol. 30, no. 2, pp. 54-60, March-April 2013, doi:10.1109/MS.2012.173.
- 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.
- Software Certification: Methods and Tools. D. Cofer, J. Hatcliff, M. Huhn, M. Lawford. Dagstuhl Seminar 13051.
- A two-level logic approach to reasoning about computations. A. Gacek, D. Miller, G. Nadathur. Journal of Automated Reasoning 49(2): 241-273 (2012).
- The Guardol language and verification system. D. Hardin, K. Slind, M. Whalen, T-H. Pham. TACAS 2012.
- The Synthesis of Cyclic Dependencies with Boolean Satisfiability. J. Backes, M. Riedel. Transactions on Design Automation of Electronic Systems, 2012.
- Compositional verification of architectural models. D. Cofer, A. Gacek, S. Miller, M. Whalen, B. LaValley, L. Sha. NASA Formal Methods, 2012, pp. 126-140.
- 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.
- Complexity-Reducing Design Patterns for Cyber-Physical Systems. D. Cofer, S. Miller, A. Gacek, M. Whalen, B. LaValley, L. Sha, A. Al-Nayeem. DARPA META Final Report.
- Nominal abstraction. A. Gacek, D. Miller, G. Nadathur. Journal Information and Computation, Volume 209 Issue 1, January, 2011 Pages 48-73.
- 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.
- Model Checking: Cleared for Take Off. D. Cofer. SPIN 2010.
- Relating nominal and higher-order abstract syntax specifications. A. Gacek. Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming (PPDP), ACM, July 2010, pp. 177-186.
- Software model checking takes off. S. Miller, M. Whalen, D. Cofer. Communications of the ACM, 2010.
- The Synthesis of Cyclic Dependencies with Craig Interpolation. J. Backes, M. Riedel. Proceedings of the International Workshop on Logic Synthesis, Berkeley, CA. 2009.
- Implementing logical synchrony in integrated modular avionics. S. Miller, D. Cofer, L. Sha, J. Meseguer, A. Al-Nayeem. DASC 2009.
- A framework for specifying, prototyping, and reasoning about computational systems. A. Gacek. Ph.D. thesis, University of Minnesota, September 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.
- The Abella interactive theorem prover (system description). A. Gacek. Proceedings of IJCAR 2008 (A. Armando, P. Baumgartner, and G. Dowek, eds.), Lecture Notes in Artificial Intelligence, vol. 5195, Springer, August 2008, pp. 154-161.
- Combining generic judgments with recursive definitions. A. Gacek, D. Miller, G. Nadathur. Proceedings of LICS 2008 (F. Pfenning, ed.), IEEE Computer Society Press, June 2008, pp. 33-44.
- Reasoning in Abella about structural operational semantics specifications. A. Gacek, D. Miller, G. Nadathur. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008) (A. Abel and C. Urban, eds.), Electronic Notes in Theoretical Computer Science, no. 228, 2008, pp. 85-100.
- Integration of Formal Analysis into a Model-Based Software Development Process. M. Whalen, D. Cofer, S. Miller, B. Krogh, W. Storm. FMICS 2007.
- The Bedwyr system for model checking over syntactic expressions. D. Baelde, A. Gacek, D. Miller, G. Nadathur, A. Tiu. 21st Conference on Automated Deduction (Frank Pfenning, ed.), LNAI, no. 4603, Springer, 2007, pp. 391-397.