# Publications

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