Publications

2024

• Towards Explainable Compositional Reasoning. I. Amundson, A. Tahat, D. Hardin, D. Cofer. 3rd International Workshop on Explainability of Real-time Systems and their Analysis (ERSA), December 2024.
• Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase. A. Tahat, D. Hardin, A. Petz, P. Alexander. AISoLA, October 2024.
• Evaluation of New Assurance Tools for Airborne Machine Learning-Based Functions. C. Liu, H. Herencia-Zapana, S. Hasan, A. Tahat, I. Amundson, D. Cofer. 43rd Digital Avionics Systems Conference, October 2024.
• Hierarchical Assurance Patterns for Cyber-Resilient Systems Engineering. I. Amundson, D. Cofer, D. Hardin, J. Hatcliff. 43rd Digital Avionics Systems Conference (DASC 2024), October 2024.
• Zero-Trust Design and Assurance Patterns for Cyber-Physical Systems. S. Hasan, I. Amundson, D. Hardin. 28th Ada-Europe International Conference on Reliable Software Technologies, June 2024.
• Transforming AADL Models Into SysML 2.0: Insights and Recommendations. K. Litwin, I. Amundson, D. Verma, T. McDermott. SAE AeroTech, March 2024.

2023

• Computer-Aided Evaluation for Argument-Based Certification. Z. Daw, T. Wang, C. Oh, M. Low, I. Amundson, G. Wang, R. Melville, P. Nuzzo. 42nd AIAA/IEEE Digital Avionics Systems Conference (DASC), 2023.
• AACE: Automated Assurance Case Environment for Aerospace Certification. Z. Daw, T. Wang, C. Oh, M. Low, I. Amundson, A. Pinto, M. Chiodo, G. Wang, S. Hasan, R. Melville, P. Nuzzo. 42nd AIAA/IEEE Digital Avionics Systems Conference (DASC), 2023.
• Computer-Aided Generation of Assurance Cases. T. Wang, C. Oh, M. Low, I. Amundson, Z. Daw, A. Pinto, M. Chiodo, G. Wang, S. Hasan, R. Melville, P. Nuzzo. 10th International Workshop on Next Generation of System Assurance Approaches for Critical Systems (SASSUR'23), 2023.
• Towards a Methodology to Design Provably Secure Cyber-physical Systems. F. Malaquias, G Giantamidis, S Basagiannis, S. F. Rollini, I. Amundson. Ada User Journal, Vol. 44(2), June 2023.
• Verifying an Aircraft Collision Avoidance Neural Network with Marabou. C. Liu, D. Cofer, D. Osipychev. NASA Formal Methods Symposium, 2023.
• Formal Methods use for Learning Assurance (ForMuLA). M. Baleani, A. Clavière, D. Cofer, E. DeWind, L. Di Guglielmo, O. Ferrante, G. Gentile, D. Kirov, D. Larsen, L. Mangeruca, S. Fulvio Rollini, G. Cima, R. Schneider, H. Semde, G. Soudain. EASA Innovation Partnership Contract, Final Report, April 2023.
• Synthesizing Verified Components for Cyber Assured Systems Engineering. E. Mercer, K. Slind, I. Amundson, D. Cofer, J. Babar, D. Hardin. Software and Systems Modeling, March 2023.
• Zero Trust Architecture Patterns for Cyber-Physical Systems. S. Hasan, I. Amundson, D. Hardin. SAE AeroTech, March 2023.
• Checking Compliance of AADL Models with Modeling Guidelines using Resolint. I. Amundson. SAE AeroTech, March 2023.
• Model-Driven Development for the seL4 Microkernel Using the HAMR Framework. J. Belt, J. Hatcliff, Robby, J. Shackleton, J. Carciofini, T. Carpenter, E. Mercer, I. Amundson, J. Babar, D. Cofer, D. Hardin, K. Hoech, K. Slind, I. Kuz, K. Mcleod. Journal of Systems Architecture, 2023.
• Autonomy Verification and Validation Roadmap and Vision 2045. G. Brat, H. Yu, E. Atkins, P. Sharma, D. Cofer, M. Durling, B. Meng, C. Alexander, S. Borgyos, C. Fan, K. Garg, U. Topcu, G. Bakirtzis. NASA Technical Report NASA/TM-20230003734, January 2023.
• Assuring Learning-Enabled Increasingly Autonomous Systems. N. Narayan, P. Ganeriwala, R. Jones, M. Matessa, S. Bhattacharyya, J. Davis, H. Purohit, S. F. Rollini. IEEE International Systems Conference (SysCon), 2023.

2022

• Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero Trust Architecture Development. D. Hardin. ACM SIGAda Ada Letters, vol. 42, no. 2, pp. 55-61, December 2022.
• Flight Test of a Collision Avoidance Neural Network with Run-Time Assurance. D. Cofer, R. Sattigeri, I. Amundson, J. Babar, S. Hasan, E. Smith, K. Nukala, D. Osipychev, M. Moser, J. Paunicka, D. Margineantu, L. Timmerman, J. Stringfield. Digital Avionics Systems Conference, September 2022.
• Model-Driven Development for the seL4 Microkernel Using the HAMR Framework. J. Belt, Robby, J. Hatcliff, J. Shackleton, J. Carciofini, T. Carpenter, E. Mercer, I. Amundson, J. Babar, D. Cofer, D. Hardin, K. Hoech, K. Slind, I. Kuz, K. Mcleod. Ada-Europe International Conference on Reliable Software Technologies, 2022.
• Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. D. Hardin. Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'22), EPTCS 359, pp. 202-216, May 2022.
• Cyber Assured Systems Engineering at Scale. D. Cofer, I. Amundson, J. Babar, D. Hardin, K. Slind, P. Alexander, J. Hatcliff, Robby, G. Klein, C. Lewis, E. Mercer, J. Shackleton. IEEE Security and Privacy, May-June 2022.
• Assume-Guarantee Reasoning with Scheduled Components. C. Liu, J. Babar, I. Amundson, K. Hoech, D. Cofer, E. Mercer. NASA Formal Methods, 2022.

2021

• Assuring Increasingly Autonomous Systems in Human-Machine Teams: An Urban Air Mobility Case Study. S. Bhattacharyya, J. Davis, A. Gupta, N. Narayan, M. Matessa. Third Workshop on Formal Methods for Autonomous Systems, October 2021.
• Synthesizing Verified Components for Cyber Assured Systems Engineering. E. Mercer, K. Slind, I. Amundson, D. Cofer, J. Babar, D. Hardin. Model-Driven Engineering Languages and Systems (MODELS), October 2021.
• Unintended Behavior in Learning-Enabled Systems: Detecting the Unknown Unknowns. D. Cofer. Digital Avionics Systems Conference, October 2021.
• Steal This Drone: DEF CON 29 Aerospace Village Activity. D. Cofer, I. Amundson, E. Barker, E. Hellman, M. Podhradsky, S. Zhuang. DEF CON Aerospace Village, August 2021.
• Specifying Message Formats with Contiguity Types. K. Slind. Interactive Theorem Proving (ITP), June 2021.
• The Assume Guarantee Reasoning Environment with Application to an Unmanned Helicopter. J. Backes, D. Cofer, I. Amundson. Technical Report. 2021.
• Resolute Assurance Arguments for Cyber Assured Systems Engineering. I. Amundson, D. Cofer. Design Automation for CPS and IoT (DESTION 2021), May 2021.
• Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. D. Hardin, K. Slind. Proceedings of the Seventh Workshop on Language-Theoretic Security at the 2021 IEEE Computer Society Security and Privacy Symposium LangSec 2021, May 2021.
• AADL-Based Safety Analysis Using Formal Methods Applied to Aircraft Digital Systems. D. Stewart, J. Liu, D. Cofer, M. Heimdahl, M. Whalen, M. Peterson. Reliability Engineering and System Safety, September 2021.
• Formal Specification and Analysis of Spacecraft Collision Avoidance Run Time Assurance Requirements. K. Hobbs, J. Davis, L. Wagner, E. Feron. 2021 IEEE Aerospace Conference.

2020

• 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.
• Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. D. Hardin. Proceedings of the 2020 IEEE Systems Conference, September 2020.
• Put Me on the RAC. D. Hardin. Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'20), May 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.
• Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel. D. Hardin, K. Slind, J. Aman Pohjola, M. Sproul. Proceedings of the 53rd Hawaii International Conference on System Sciences, January 2020.

2019

• When Human Intuition Fails: Using Formal Methods to Find an Error in the 'Proof' of a Multi-Agent Protocol. J. Davis, D. Kingston, L. Humphrey. CAV 2019.
• Model-Based Grey-Box Fuzzing. D. Greve. 19th High Confidence Software and Systems Conference (HCSS), April 2019.

2018

• 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.

2017

• 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.

2016

• 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.

2015

• 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.

2014

• 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.

2013

• 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.

2012

• 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.

2011

• 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.

2010

• 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.

2009

• 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.

2008

• 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.

2007

• 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.

2006

• The suspension calculus and its relationship to other explicit treatments of substitution in lambda calculi. A. Gacek. Master's thesis, University of Minnesota, December 2006.