LFM Publications

2024

James Chamberlain, Maria Consiglio, César Muñoz, and Paolo Masci, Assistive detect and avoid technology in urban air mobility environments, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

Paolo Masci, James Chamberlain, César Muñoz, and Maria Consiglio, DANTi: A tool for assistive detect and avoid research, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

J Tanner Slagel, Lauren M. White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A verification framework for runtime assurance of autonomous UAS, Proceedings of the 43rd Digital Avionics Systems Conference (DASC 2024), September-October 2024, San Diego, CA, USA. BibTeX Reference.

Laura R. Humphrey and César A. Muñoz, Preliminary application of formal verification to an autonomy architecture for unmanned aircraft, Proceedings of the 34th International Congress of the Aeronautical Sciences (ICAS 2024), 2024. BibTeX Reference.

Laura Titolo, Mariano Moscato, Marco Feliu, Paolo Masci, and César Muñoz, Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0, Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Lecture Notes in Computer Science, Vol. 14934, pp. 20-38. BibTeX Reference.

J Tanner Slagel, Lauren White, Aaron Dutle, César Muñoz, and Nicolas Crespo, A Formal Verification Framework for Runtime Assurance, Proceedings of the 16th NASA Formal Methods Symposium (NFM 2024), Lecture Notes in Computer Science, Vol. 14627, pp. 322-328. BibTeX Reference.

Lauren White, Laura Titolo, J Tanner Slagel, and César Muñoz, A Temporal Differential Dynamic Logic Formal Embedding, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), London, UK, 2024. BibTeX Reference.

2023

César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Journal of Automated Reasoning, Volume 67, Number 4, 2023. BibTeX Reference. This paper is an extended version of the conference publication in Schloss Dagstuhl - Leibniz- Zentrum für Informatik, Article No. 26, pp. 1-17, 2021.

Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, Mauricio Ayala-Rincón, A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023), pp. 237-246, TU Wien Academic Press, 2023. BibTeX Reference.

Víctor Carreño, ATM-X Urban Air Mobility: Assistive Detect and Avoid for UAM Operations Safety Evaluation Metrics, Contractor Report, NASA/CR-20230013203, December 2023. BibTeX Reference.

Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez, editors, Selected Extended Papers of NFM 2021, Special Issue, Innovations in Systems and Software Engineering, Vol. 19, Issue 4, Springer, 2023.

J Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran, and Aaron Dutle, Embedding Differential Dynamic Logic in PVS,Proceedings of the 18th International Workshop on Logical and Semantic Frameworks, with Applications, 2023. BibTeX Reference.

Lauren White, Laura Titolo, J Tanner Slagel, Embedding Differential Temporal Dynamic Logic in PVS, Proceedings of the 29th International Conference on Types for Proofs and Programs TYPES 2023, 2023. Abstract.

2022

Paolo Masci, Formal Analysis of the Application Programming Interface of the PVS Verification System, Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 128, 2022. BibTeX Reference.

J Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, and Lauren White, Towards an implementation of differential dynamic logic in PVS, Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), 2022.. BibTeX Reference.

Víctor Carreño, Paolo Masci, Maria Consiglio, Assistive Detect-and-Avoid for Pilots in the Cockpit, Proceedings of the 41st Digital Avionics Systems Conference (DASC 2022), September 2022, Portsmouth, VA, USA. BibTeX Reference.

Víctor Carreño, Mariano M. Moscato, Paolo M. Masci, and Aaron Dutle, Interpretation and formalization of the right-of-way rules, Proceedings of 18th International Conference on Formal Aspects of Component Software (FAC 2022), Lecture Notes in Computer Science, Vol. 13712, pp. 59-73, 2022. BibTeX Reference.

Paolo Masci and Aaron Dutle, Proof Mate: an Interactive Proof Helper for PVS (tool paper), Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Lecture Notes in Computer Science, Vol. 13260, pp. 809-815, 2022. BibTeX Reference.

Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle, A Compositional Proof Framework for FRETish Requirements, Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), 2022. BibTeX Reference.

2021

J Tanner Slagel, Lauren White, and Aaron Dutle, Formal verification of semi-algebraic sets and real analytic functions, Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proof, pp. 278-290, 2021. BibTeX Reference.

Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot, Formal Analysis of the Compact Position Reporting Algorithm, Formal Aspects of Computing, Volume 33, Number 1, pp. 65-86, 2021. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018.

Andrew Peters, Brendan Duffy, Swee Balachandran, María Consiglio, and César Muñoz, SIRIUS: Simulation Infrastructure for Research on Interoperating Unmanned Systems, Proceedings of the 40th Digital Avionics Systems Conference (DASC 2021), Virtual Conference, US, 2021. BibTeX Reference.

César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, and Thiago M. Ferreira, Formal Verification of Termination Criteria for First-Order Recursive Functions, Proceedings of the 12th International Conference on Interactive Theorem Proving (ITP 2021), Article No. 26, pp. 1-17, Schloss Dagstuhl - Leibniz- Zentrum für Informatik, 2021. BibTeX Reference

Katherine Cordwell, César Muñoz, and Aaron Dutle, Improving automated strategies for univariate quantifier elimination, Technical Memorandum, NASA/TM-20205010644, January 2021. BibTeX Reference.

Aaron Dutle, Mariano M. Moscato, Laura Titolo, César Muñoz, and Ivan Perez, editors, Proceedings of the 13th International Symposium, NFM 2021, Virtual Event, May 24–28, 2021, Lecture Notes in Computer Science, Volume 12673, Springer, 2021.

2020

Laura Titolo, Mariano Moscato, Marco Feliú, and César Muñoz, Automatic Generation of Guard-Stable Floating-Point Code, Proceedings of the 16th International Conference on Integrated Formal Methods (iFM 2020), Lecture Notes in Computer Science, Vol. 12546, pp. 141–159, 2020. BibTeX Reference.

Aaron Dutle, César Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, and Thomas Pressburger, From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project, Proceedings of the Second Workshop on Formal Methods for Autonomous Systems (FMAS 2020), Electronic Proceedings in Theoretical Computer Science, Vol. 329, pp. 23–30, 2020. BibTeX Reference.

Andrew Peters, Swee Balachandran, Brendan Duffy, Kyle Smalling, María Consiglio, and César Muñoz, Flight Test Results of a Distributed Merging Algorithm for Autonomous UAS Operations, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Brendan Duffy, Swee Balachandran, Andrew Peters, Kyle Smalling, María Consiglio, Louis Glaab, Andrew Moore, and César Muñoz, Onboard Autonomous Sense and Avoid of Non-Conforming Unmanned Aerial Systems, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Sami Mian, Tyler Garrett, Alexander Glandon, Christopher Manderino, Swee Balachandran, César Muñoz, and Chester Dolph, Autonomous Spacecraft Inspection with Free-Flying Drones, Proceedings of the 39th Digital Avionics Systems Conference (DASC 2020), Virtual Conference, US, 2020. BibTeX Reference.

Swee Balachandran, Christopher Manderino, César Muñoz, and María Consiglio, A Decentralized Framework to Support UAS Merging and Spacing Operations in Urban Canyons, Proceedings of 2020 International Conference on Unmanned Aircraft Systems (ICUAS 2020), 2020. BibTeX Reference.

Brendon K. Colbert, J Tanner Slagel, Luis G. Crespo, Swee Balachandran, and César Muñoz, PolySafe: A Formally Verified Algorithm for Conflict Detection on a Polynomial Airspace, Proceedings of 1st Virtual IFAC World Congress (IFAC-V 2020), 2020. BibTeX Reference.

Paolo Masci and César Muñoz, A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems, Proceedings of the 14th International Conference on Tests and Proofs (TAP 2020), Lecture Notes in Computer Science, Vol. 12165, pp. 155-166, 2020. BibTeX Reference.

Brendan Duffy, Swee Balachandran, María Consiglio, Louis Glaab, César Muñoz, Kyle Smalling, Nicholas Rymer, David Bradley, David Hare, Richard Grube, Matthew Coldsnow, Scott Sims, Jeffrey Hill, and Mahyar Malekpour, Sense and Avoid Characterization of the ICAROUS Architecture , Technical Memorandum, NASA/TM-2020-220591, May 2020. BibTeX Reference.

2019

Aaron Dutle, César Muñoz, and Anthony Narkawicz, editors, Selected Extended Papers of NFM 2018, Special Issue, Innovations in Systems and Software Engineering, Vol. 15, Issues 3-4, Springer, 2019.

Mauricio Ayala-Rincón and César Muñoz, editors, Selected Extended Papers of ITP 2017, Special Issue, Journal of Automated Reasoning, Vol. 63, Issue 2, Springer, 2019.

2018

Laura Titolo, Marco Feliu, Mariano Moscato, and César Muñoz, An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs, 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018), Lecture Notes in Computer Science, Vol. 10747, pp. 516-537, January 2018. BibTeX Reference.

Aaron Dutle, César Muñoz, and Anthony Narkawicz, editors, Proceedings of the 10th International Symposium, NFM 2018, Newport News, Virginia, USA, April 17–19, 2018, Lecture Notes in Computer Science, Volume 10811, Springer, 2018.

2017

Andrew J. Moore, Matthew Schubert, Nicholas Rymer, Swee Balachandran, María Consiglio, César A. Muñoz, Joshua Smith, Dexter Lewis, Paul Schneider, UAV Inspection of Electrical Transmission Infrastructure with Path Conformance Autonomy and Lidar-based Geofences NASA Report on UTM Reference Mission Flights at Southern Company Flights November 2016, Technical Memorandum, NASA/TM-2017-219673, October 2017. BibTeX Reference.

George E. Hagen, Nelson M. Guerreiro, Jeffrey M. Maddalon, Ricky W. Butler. An effcient Universal Trajectory Language, NASA/TM-2017-219669, Sept 2017.

Mariano Moscato, Laura Titolo, Aaron Dutle, and César Muñoz, Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis, Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017), Lecture Notes in Computer Science, Vol. 10488, pp. 213-229, August 2017. BibTeX Reference.

Aaron Dutle, Mariano Moscato, Laura Titolo, and César Muñoz, A Formal Analysis of the Compact Position Reporting Algorithm , Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), Lecture Notes in Computer Science, Vol. 10712, pp. 19-34, July 2017. BibTeX Reference.

Swee Balachandran, César Muñoz, and María Consiglio, Implicitly Coordinated Detect and Avoid Capability for Safe Autonomous Operation of Small UAS, Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), AIAA-2017-4484, June 2017. BibTeX Reference.

James Chamberlain, María Consiglio, and César Muñoz, DANTi: Detect and Avoid iN The Cockpit, Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), AIAA-2017-4491, June 2017. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, The MINERVA Software Development Process, Automated Formal Methods, Menlo Park, California, 2017. BibTeX Reference.

Camilo Rocha, José Meseguer, and César Muñoz, Rewriting Modulo SMT and Open System Analysis, Journal of Logical and Algebraic Methods in Programming, Volume 86, Issue 1, pp. 269–297, January 2017.. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 8663, pp. 247-262, 2014.

Rania W. Ghatas, Devin P. Jack, Dimitrios Tsakpinis and Michael J. Vincent, James L. Sturdy, César A. Muñoz, Keith D. Hoffler, Aaron M. Dutle, Robert Myer, Anna M. DeHaven and Tod Lewis, and Keith E. Arthur, Unmanned Aircraft Systems Minimum Operational Performance Standards End-to-End Verification and Validation (E2-V2) Simulation, Technical Memorandum, NASA/TM-2017-20780, January 2017. BibTeX Reference.

Mauricio Ayala-Rincón and César Muñoz, editors, Proceedings of the 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Lecture Notes in Computer Science, Volume 10499, Springer, 2017.

César Muñoz, Sanjai Rayadurgam, and Oksana Tkachuk, editors, Selected Extended Papers of NFM 2016, Special Issue, Journal of Automated Reasoning, Springer, 2017.

... 2016

María Consiglio, César Muñoz, George Hagen, Anthony Narkawicz, and Swee Balachandran, ICAROUS: Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems, Proceedings of the 35th Digital Avionics Systems Conference (DASC 2016), Sacramento, California, Sept 2016. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Aaron Dutle, Coordination Logic for Repulsive Resolution Maneuvers, Proceedings of the 16th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2016), AIAA-2016-2756, Washington D.C., June 2016. BibTeX Reference.

Hagen, George E., Butler, Ricky W., Maddalon, Jeffrey M. The Stratway Program for Strategic Conflict Resolution: User's Guide , NASA/TM-2016-219196, May 2016.

James Comstock, Rania Ghatas, Michael Vincent, María Consiglio, César Muñoz , James Chamberlain, Paul Volk, and, Keith Arthur, Unmanned Aircraft Systems Human-in-the-Loop Controller and Pilot Acceptability Study: Collision Avoidance , Self-Separation, and Alerting Times (CASSAT), Technical Memorandum, NASA/TM-2016-219181, April 2016. BibTeX Reference.

Nelson M. Guerreiro, Ricky W. Butler, George E. Hagen, Jeffrey M. Maddalon, and Timothy A. Lewis Parametric Analysis of Surveillance Quality and Level and Quality of Intent Information and their Impact on Conflict Detection Performance, NASA/TM-2016-219177, March 2016.

César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain, DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.

María Consiglio, César Muñoz, George Hagen, Anthony Narkawicz, Jason Upchurch, James Comstock, Rania Ghatas, Michael Vincent, and James Chamberlain, Human-In-The-Loop Experimental Research for Detect and Avoid, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.

Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions, Air Traffic Control Quarterly, Vol 23(4) pp. 275-299, 2015. BibTeX Reference. Also appeared as Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions (Best paper of track award), Proceedings of the 11th USA/Europe Air Traffic Management R&D Seminar, ATM 2015, Lisbon, Portugal, 2015. BibTeX Reference.

James Chamberlain, María Consiglio, James Comstock, Rania Ghatas, and César Muñoz, NASA Controller Acceptability Study 1 (CAS-1) Experiment Description and Initial Observations, Technical Memorandum, NASA/TM-2015-218763, May 2015. BibTeX Reference.

Anthony Narkawicz and César Muñoz, A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories, Proceedings of the 2015 AIAA Infotech @ Aerospace Conference, AIAA-2015-0795, Kissimmee, Florida, 2015. BibTeX Reference.

César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain, DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems, Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015), Prague, Czech Republic, 2015. BibTeX Reference.

Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions, Air Traffic Control Quarterly, Vol 23(4) pp. 275-299, 2015. BibTeX Reference. Also appeared as Jason Upchurch, César Muñoz, Anthony Narkawicz, María Consiglio, and James Chamberlain, Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions (Best paper of track award), Proceedings of the 11th USA/Europe Air Traffic Management R&D Seminar, ATM 2015, Lisbon, Portugal, 2015. BibTeX Reference.

Anthony Narkawicz and César Muñoz, A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories, Proceedings of the 2015 AIAA Infotech @ Aerospace Conference, AIAA-2015-0795, Kissimmee, Florida, 2015. BibTeX Reference.

George E. Hagen and Ricky W. Butler, Towards a Formal Semantics of Flight Plans and Trajectories, NASA/TM–2014-218662, Dec 2014.

Jason Upchurch, César Muñoz, Anthony Narkawicz, James Chamberlain, and María Consiglio, Analysis of Well-Clear Boundary Models for the Integration of UAS in the NAS, Technical Memorandum, NASA/TM-2014-218280, June 2014. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and George Hagen, An Independent and Coordinated Criterion for Kinematic Aircraft Maneuvers, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2859, Atlanta, Georgia, 2014. BibTeX Reference.

César Muñoz, Anthony Narkawicz, James Chamberlain, María Consiglio, and Jason Upchurch, A Family of Well-Clear Boundary Models for the Integration of UAS in the NAS, Proceedings of the 14th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2014-2412, Atlanta, Georgia, 2014. BibTeX Reference.

Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, and César Muñoz, Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol, Proceedings of the 19th International Symposium on Formal Methods (FM 2014), Lecture Notes in Computer Science, Vol. 8442, pp. 215-229, 2014. BibTeX Reference.

Anthony Narkawicz, César Muñoz, Jason Upchurch, James Chamberlain, and María Consiglio, A Well-Clear Volume Based on Time to Entry Point, Technical Memorandum, NASA/TM-2014-218155, January 2014. BibTeX Reference.

Wilfredo Torres-Pomales, Michael M. Madden, Ricky W. Butler, and Raleigh B. Perry, Analysis and Simulation of the Simplified Aircraft-Based Paired Approach Concept With the ALAS Alerting Algorithm in Conjunction With Echelon and Offset Strategies NASA/TM–2014-218151, Jan 2014.

César Muñoz, Anthony Narkawicz, and James Chamberlain, A TCAS-II Resolution Advisory Algorithm, Proceedings of the AIAA Guidance, Navigation, and Control Conference (GNC), AIAA-2013-4622, Boston, Massachusetts, August 2013. BibTeX Reference.

Anthony Narkawicz, César Muñoz, Heber Herencia-Zapana, and George Hagen, Formal Verification of Lateral and Temporal Safety Buffers for State-Based Conflict Detection, Proceedings of the Institution of Mechanical Engineers, Part G: Journal of Aerospace Engineering, Vol. 227, No. 9, pp. 1412-1424, September 2013. BibTeX Reference.

Ricky W. Butler, George E. Hagen, and Jeffrey M. Maddalon The Chorus Conflict and Loss of Separation Resolution Algorithms, NASA/TM–2013-218030, August 2013.

Raleigh B. Perry, Michael M. Madden, Wilfredo Torres-Pomales, and Ricky W. Butler, The Simplified Aircraft-Based Paired Approach with the ALAS Alerting Algorithm, NASA/TM-2013-217804, Feb 2013.

Anthony Narkawicz and César Muñoz, Formal Verification of Conflict Detection Algorithms for Arbitrary Trajectories, Reliable Computing, Volume 17, pp. 209-237, December, 2012. BibTeX Reference.

Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, and Anthony Narkawicz, The search for effective algorithms for recovery from loss of separation, Proceedings of the 31st Digital Avionics Systems Conference (DASC 2012), Williamsburg, Virginia, 2012. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Jeffrey Maddalon, A Mathematical Analysis of Air Traffic Priority Rules, Proceedings of the 12th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, AIAA-2012-5544, Indianapolis, Indiana, 2012. BibTeX Reference.

María Consiglio, James Chamberlain, César Muñoz, and Keith Hoffler, Concept of integration for UAS operations in the NAS, Proceedings of the 28th International Congress of the Aeronautical Sciences (ICAS 2012), 2012. BibTeX Reference.

Anthony Narkawicz, César Muñoz, and Gilles Dowek, Provably Correct Conflict Prevention Bands Algorithms, Science of Computer Programming, Volume 77, Issues 10-11, pp. 1039-1057, September 2012. BibTeX Reference.

Anthony Narkawicz and César Muñoz, State-based implicit coordination and applications, Technical Publication, NASA/TP-2011-217067, March 2011. BibTeX Reference.

Anthony Narkawicz, A Formal Proof Of The Riesz Representation Theorem, Journal of Formalized Reasoning, Vol 4, No. 1, 2011. BibTeX Reference.

Hagen, G. E.; Butler, R. W.; and Maddalon, J. M.: Stratway: A Modular Approach to Strategic Conflict Resolution. Presented at 11th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference, September 20-22, 2011, Virginia Beach, Virginia.

Luis Crespo, César Muñoz, Anthony Narkawicz, Sean Kenny, and Daniel Giesy, Uncertainty Analysis via Failure Domain Characterization: Polynomial Requirement Functions, European Safety and Reliability Conference, September 2011. BibTeX Reference.

Heber Herencia-Zapana, George Hagen, and Anthony Narkawicz, Formalizing Probabilistic Safety Claims, Third NASA Formal Methods Symposium, April 2011. BibTeX Reference.

Anthony Narkawicz and César Muñoz, State-based implicit coordination and applications, Technical Publication, NASA/TP-2011-217067, March 2011. BibTeX Reference.

Hélène Kirchner and César Muñoz, editors, Proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming, EPTCS Vol. 44, 2010. BibTex Reference.

César Muñoz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George Hagen, A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing the Safety of Self-Separation in NextGen, Technical Memorandum, NASA/TM-2010-216862, October 2010. BibTeX Reference.

César Muñoz and Anthony Narkawicz, Time of Closest Approach in Three-Dimensional Airspace, Technical Memorandum, NASA/TM-2010-216857, October 2010. BibTeX Reference.

Heber Herencia-Zapana, Jean-Baptiste Jeannin, and César Muñoz, Formal Verification of Safety Buffers for State-Based Conflict Detection and Resolution, Proceedings of the of 27th International Congress of the Aeronautical Sciences (ICAS 2010), 2010.

Anthony Narkawicz, César Muñoz, and Gilles Dowek, Formal verification of air traffic prevention bands algorithms, Technical Memorandum, NASA/TM-2010-216706, June 2010.

César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA/CP-2010-216215, 2010.

Florent Kirchner and César Muñoz, The Proof Monad, Journal of Logic and Algebraic Programming, Vol 79 (3-5), pp. 264-277, 2010.

Ricky W. Butler; George Hagen; Jeffrey M. Maddalon; César A. Muñoz; Anthony Narkawicz; How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project, Second NASA Formal Methods Symposium (NFM 2010), Washington D.C., April 13-15, 2010.

Jeffrey Maddalon, Ricky Butler, César Muñoz, and Gilles Dowek, Mathematical Basis for the Safety Analysis of Conflict Prevention Algorithms, Technical Memorandum, NASA TM-2009-215768, June 2009. BibTex Reference.

Butler, Ricky W.; Muñoz, César A. Formally Verified Practical Algorithms For Recovery From Loss of Separation , NASA TM-2009-215726, June 2009.

Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover , Journal of Formalized Reasoning, Vol 2, No 1., 2009.

Butler, Ricky W.; Muñoz, César A. A Formal Framework for the Analysis of Algorithms That Recover From Loss of Separation , NASA TM-2008/215356, Oct 2008.

Radu Siminiceanu, Ricky W. Butler, César A. Muñoz: Experimental Evaluation of a Planning Language Suitable for Formal Verification", Model Checking and Artificial Intelligence 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008; Lecture Notes in Computer Science, Springer Berlin, Volume 5348/2009.

Ricky W. Butler, A Primer on Architectural Level Fault Tolerance, NASA/TM-2008-215108, Feb 2008.

Ricky Butler, Radu Siminiceanu and César Muñoz, The ANMLite Language and Logic for Specifying Planning Problems, NASA/TM-2007-215089 , Nov 2007.

Ricky Butler, César Muñoz, and Radu Siminiceanu, Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL), NASA/TM-2007-215089 , Nov 2007.

Kelly J. Hayhurst, Jeffrey M. Maddalon, Paul S. Miner, George N. Szatkowski, Michael L. Ulrey, Michael P. DeWalt, Cary R. Spitzer. Preliminary Considerations for Classifying Hazards of Unmanned Aircraft Systems. NASA Technical Memorandum (TM-2007-214539), February 2007.

Ricky Butler and César Muñoz, An Abstract Plan Preparation Language, NASA/TM-2006-214518, Nov 2006.

Hayhurst, Kelly J.; Maddalon, Jeffrey M.; Miner, Paul S.; DeWalt, Michael P.; McCormick, G. Frank Unmanned Aircraft Hazards and their Implications for Regulation , 15-19 Oct. 2006; 25th Digital Avionics Systems Conference; Portland, Oregon.

Songtao Xia, Ben Di Vito and César Muñoz. Predicate Abstraction of Programs Containing Non-linear Computation. In ATVA 2006, Fourth International Symposium on Automated Technology for Verification and Analysis, Beijing, China, October 2006.

T. Pressburger, L. Markosian, B. Di Vito, M. Feather, M. Hinchey and L. Treviño. Infusing Software Assurance Research Techniques into Use. In IEEE 2006 Aerospace Conference, IEEE, Big Sky, MT, March 2006.

Songtao Xia, Ben Di Vito and César Muñoz. Automated Test Generation for Engineering Applications. In Automated Software Engineering 2005, ACM, Long Beach, CA, November 2005.

Songtao Xia and Ben Di Vito. Software Certification for Temporal Properties with Affordable Tool Qualification. In Workshop on Software Certificate Management (SoftCeMent), Long Beach, CA, November 2005.

Lee Pike and Steven D. Johnson. The formal verification of a reintegration protocol. Accepted at the ACM Conference on Embedded Software (EMSOFT), 2005.

Holloway, C. Michael; Johnson, Chris W.: On the Prevalence of Organizational Factors in Recent U.S. Transportation Accidents, to appear in Proceedings of the 23rd International System Safety Conference, 22-26 August 2005, San Diego, California.

Johnson, Chris W.; Holloway, C. Michael: "A Technique for Showing Causal Arguments in Accident Reports", to appear in Proceedings of the 23rd International System Safety Conference, 22-26 August 2005, San Diego, California.

Lee Pike. Real-time system verification by k-induction. NASA Technical Memorandum TM-2005-213751, April 2005.

Wilfredo Torres-Pomales, Mahyar R. Malekpour, and Paul S. Miner.  ROBUS-2: A fault-tolerant broadcast communication system.  NASA/TM-2005-213540, March 2005, pp. 201.

Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser. Abstractions for fault-tolerant distributed system verification. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 257--270. Springer, 2004.

Lee Pike, Paul Miner, Wilfredo Torres. Model Checking Failed Conjectures in Theorem Proving: A Case Study. NASA Technical Memorandum NASA/TM-2004-213278, October 2004.
Proof files are available here.

Victor Carreño and César Muñoz, Implicit Intent Information for Conflict Detection and Alerting, Proceedings of the 23th Digital Avionics Systems Conference, DASC 2004, Salt Lake City, Utah, October 2004.

Ricky Butler, Formalization of the Integral Calculus in the PVS Theorem Prover , NASA TM-2004-213279,Oct-2004.

Paul Miner, Alfons Geser, Lee Pike, and Jeffrey Maddalon. A Unified Fault-tolerance Protocol.In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of Lecture Notes in Computer Science, pages 167--182. Springer, 2004.

M. Consiglio, C. Muñoz, and V. Carreño, Conflict Detection and Alerting in a Self Controlled Terminal Aerospace, 24th International Congress of the Aeronautical Sciences, Yokohama, Japan, August 2004.

Johnson, Chris W.; Holloway, C. Michael: "`Systemic Failures' and `Human Error' in Canadian TSB Aviation Accident Reports between 1996 and 2002," Proceedings of HCI in Aerospace 2004, 29 September - 1 October 2004, Toulouse, France.

Holloway, C. Michael; Johnson, Chris W.: "Distribution of Causes in Selected U.S. Aviation Accident Reports Between 1996 and 2003," Proceedings of the 22nd International System Safety Conference, 2-6 August 2004, Providence, Rhode Island.

César Muñoz, Gilles Dowek, and Victor Carreño, Modeling and Verification of an Air Traffic Concept of Operations, International Symposium on Software Testing and Analysis, Boston, Massachusetts, July 2004.

Jeffrey Maddalon, Ricky Butler, Alfons Geser and César Muñoz, Formal Verification of a Conflict Resolution and Recovery Algorithm , NASA/TP-2004-213015, April 2004, pp. 82.

Gerard Allwein, Hilmi Demir, Lee Pike, Logics for Classes of Boolean Monoids, Journal of Logic, Language and Information.  13-3: 2004 (Kluwer).  pp. 241-266.

Gilles Dowek, César A. Muñoz, and Victor Carreño, An Abstract Model of the SATS Concept of Operations: Initial Results and Recommendations, NASA/TM-2004-213006, March 2004.

Victor A. Carreno, Hanne Gottliebsen, Ricky Butler and Sara Kalvala, Formal Modeling and Analysis of a Preliminary Small Aircraft Transportation System (SATS) Concept, NASA/TM-2004-212999, March 2004, pp. 44.

Paul Miner, Alfons Geser, Lee Pike, and Jeffery Maddalon. A unified fault-tolerance protocol. In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems (FORMATS-FTRTFT), volume 3253 of Lecture Notes in Computer Science, pages 167--182. Springer, 2004. Proof files are available here.

Lee Pike, Jeffery Maddalon, Paul Miner, and Alfons Geser. Abstractions for fault-tolerant distributed system verification. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 3223 of Lecture Notes in Computer Science, pages 257--270. Springer, 2004.  Proof files are available here.

Elizabeth Latronico, Paul Miner, and Philip Koopman. Quantifying the Reliability of Proven SPIDER Group Membership Service Guarantees. Dependable Systems and Networks (DSN), 2004. 

Ricky Butler, Alfons Geser, Jeffrey Maddalon, and César Muñoz: Formal Analysis of Air Traffic Management Systems: The case of Conflict Resolution and Recovery, Proceedings of Winter Simulation Conference (WSC'03), New Orleans, December 2003, pp. 906-914, ISBN 0-7803-8132-7.

Johnson, Chris W.; Holloway, C. Michael: "The ESA/NASA SOHO Mission Interruption: Using the STAMP Accident Analysis Technique for a Software Related `Mishap'", Software: Practice and Experience, Volume 33, Number 12, October 2003, pp. 1177-1198.

Victor A. Carreno: Concept for Multiple Operations at Non-Tower Non-Radar Airports During Instrument Meteorological Conditions, Proceeding of the 22nd Digital Avionics Systems Conference, DASC 2003, Indianapolis, Indiana, 12-16 October 2003.

Hayhurst, Kelly J.; Holloway, C. Michael: "Considering Object Oriented Technology in Aviation Applications", Proceedings of the 22nd Digital Avionics Systems Conference, 12-16 October 2003, Indianapolis, Indiana, paper 3.B.1.

Ben L. Di Vito: Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS, 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Roma, Italy, September 8, 2003.

M. Archer, B. Di Vito and C. Muñoz, editors. Design and Application of Strategies/Tactics in Higher Order Logics. NASA Conference Publication NASA/CP-2003-212448, NASA Langley Research Center, Hampton, VA, September 2003.

César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek: Formal verification of conflict detection algorithms, International Journal on Software Tools for Technology Transfer, 2003.

Proceedings of the Second Workshop on the Investigation and Reporting of Incidents and Accidents (IRIA 2003), NASA/CP-2003-212642, Kelly J. Hayhurst and C. Michael Holloway (compilers), September 2003.

Holloway, C. Michael; Hayhurst, Kelly J.: "Software System Safety & the NASA Aeronautics Blueprint", Proceedings of the 21st International System Safety Conference, 4-8 August 2003, Ottawa, Ontario, Canada, pp. 1183-1192.

Johnson, Chris W.; Holloway, C. Michael: "The Strengths and Weaknesses of Logic Formalisms to Support Mishap Analysis", Proceedings of the 21st International System Safety Conference, 4-8 August 2003, Ottawa, Ontario, Canada, pp. 1133-1142.

Johnson, Chris W.; Holloway, C. Michael: A Survey of Logic Formalisms to Support Mishap Analysis, Reliability Engineering and Systems Safety, Volume 80, Issue 3, June 2003, pp 271-291.

Jeffrey M. Maddalon and Paul S. Miner: An Architectural Concept for Intrusion Tolerance in Air Traffic Networks, 3rd Integrated Communications, Navigation, and Surveillance (ICNS) Conference & Workshop, Annapolis, Maryland, May 19-22, 2003.

Victor A. Carreño, Evaluation of a Pair-Wise Conflict Detection and Resolution Algorithm in a Multiple Aircraft Scenario December 2002.

Alfons Geser and Paul Miner.   A New On-line Diagnosis Protocol for the SPIDER Family of Byzantine Fault Tolerant Architectures .  NASA TM, 2003.

Hayhurst, Kelly J; Holloway, C. Michael: "Aviation Software Guidelines", IEEE Software, Volume 19, Number 5, Sep/Oct 2002.

Holloway, C. Michael: " Issues in Software System Safety: Polly Ann Smith Co. v. Ned I. Ludd", in the Proceedings of the 20th International System Safety Conference, Aurora, CO, 5-9 August 2002, pp. 75-84.

Victor A. Carreño, César Muñoz, and Sofiéne Tahar, Eds., Theorem Proving in Higher Order Logics Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, NASA/CP-2002-211736, August 2002, pages 198.

Ben L. Di Vito: A PVS Prover Strategy Package for Common Manipulations, NASA/TM-2002-211647, April 2002.

Alfons Geser, Paul Miner.   A Formal Correctness Proof of the SPIDER Diagnosis Protocol .  Theorem-Proving in Higher-Order Logics (TPHOLs), track B, 2002.

Paul S. Miner, Mahyar R. Malekpour, Wilfredo Torres.  A Conceptual Design For a Reliable Optical Bus (ROBUS).  Presented at the 21st Digital Avionics Systems Conference (DASC), Irvine, California, October 27-31, 2002.

NASA Langley's Research and Technology Transfer Program in Formal Methods, 2002 (PostScript and PDF). It is out of date.

Hayhurst, Kelly J; Holloway, C. Michael: "Challenges in Software Aspects of Aviation Systems", in the Proceedings of the 26 Annual NASA Goddard Software Engineering Workshop (IEEE/NASA SEW-26), 27-29 November 2001, Greenbelt, MD, pp. 7-13.

Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson, A Practical Tutorial on Modified Condition/Decision Coverage NASA/TM-2001-210876, NASA Langley Research Center,Hampton, Virginia, May 2001.

César Muñoz, Ricky W. Butler,Victor A. Carreño, and Gilles Dowek. On the Formal Verification of Conflict Detection Algorithms, NASA/TM-2001-210864, May 2001.

César Muñoz, Ricky Butler, Víctor Carreño, and Gilles Dowek, Verification of Conflict Detection Algorithms, Proceedings of the 11th Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001. Extended version available as NASA/TM-2001-210864.

Victor Carreño and César Muñoz, Formal Analysis of Parallel Landing Scenarios Proceedings of the 19th Digital Avionics Systems Conference, DASC 2000. (PostScript).

Carreno, Victor and César Muñoz, Aircraft trajectory modeling and alerting algorithm verification , ICASE Report 2000-16, 2000-04-01.

C. Michael Holloway (compiler). Lfm2000: Fifth NASA Langley Formal Methods Workshop. NASA/CP-2000-210100, NASA Langley Research Center, Hampton, Virginia, June 2000.

Kelly J. Hayhurst, Cheryl A. Dorsey, John C. Knight, Nancy G. Leveson and G. Frank McCormick, Streamlining Software Aspects of Certification: Report on the SSAC Survey, NASA/TM-1999-209519, August 1999, 100 pages. Information on the SSAC project is here.

C. Michael Holloway: From Bridges and Rockets, Lessons for Software Systems, in the Conference Proceedings of the 17th International System Safety Conference, August 16-21, 1999, Orlando, Florida, pages 598-607.

Luettgen, Gerald; Carreno, Victor: Analyzing mode confusion via model checking , ICASE Report 99-18, 1999-05-01.

Steven P. Miller and James N. Potts. Detecting Mode Confusion Through Formal Modeling and Analysis. NASA Contractor Report CR-1999-208971, January 1999, 69 pages.

Ben L. Di Vito. A Model of Cooperative Noninterference for Integrated Modular Avionics. In Proceedings of Dependable Computing for Critical Applications (DCCA-7), San Jose, CA, January 1999.

Ricky W. Butler, Steven P. Miller, James N. Potts, and Victor A. Carreño. A Formal Methods Approach to the Analysis of Mode Confusion. In 17th AIAA/IEEE Digital Avionics Systems Conference, October 31-November 6 1998.

Ben L. Di Vito. A Formal Model of Partitioning for Integrated Modular Avionics. NASA Contractor Report CR-1998-208703, NASA Langley Research Center, Hampton, Virginia, August 1998.

Kelly J. Hayhurst. Framework for Small-Scale Experiments in Software Engineering. NASA Technical Memorandum TM-1998-207666, NASA Langley Research Center, Hampton, Virginia, May 1998.

K. J. Hayhurst, C. M. Holloway, C. A. Dorsey, J. C. Knight, N. G. Leveson, G. F. McCormick, and J. C. Yang. Streamlining Software Aspects of Certification: Technical Team Report on the First Industry Workshop. NASA Technical Memorandum TM-1998-207648, NASA Langley Research Center, Hampton, Virginia, April 1998. Information on the SSAC project is here.

Ricky W. Butler and J. A. Sjogren. A PVS Graph Theory Library. NASA Technical Memorandum TM-1998-206923, NASA Langley Research Center, Hampton, Virginia, February 1998.

C. Michael Holloway. Why Engineers Should Consider Formal Methods. In 16th AIAA/IEEE Digital Avionics Systems Conference, Volume 1, pages 1.3-16 -- 1.3-22, October 26-30 1997. Presentation slides are available.

C. Michael Holloway and Kelly J. Hayhurst (compilers). Lfm97: Fourth NASA Formal Methods Workshop. NASA Conference Publication 3356, NASA Langley Research Center, Hampton, Virginia, September 1997.

Ben L. Di Vito. Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request. NASA Contractor Report 4752, NASA Langley Research Center, Hampton, Virginia, August 1996.

Ricky W. Butler. An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot. NASA Technical Memorandum 111025, NASA Langley Research Center, Hampton, Virginia, May 1996. ( Revised Paper(PostScript))

C. Michael Holloway and Ricky W. Butler. Impediments to Industrial Use of Formal Methods. IEEE Computer, 29(4):25-26, April 1996.

Ben L. Di Vito. Formalizing New Navigation Requirements for NASA's Space Shuttle. In Formal Methods Europe (FME '96), pages 160-178, Oxford, England, March 1996. Also Lecture Notes in Computer Science 1051, Springer.

Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle Software Requirements. In Workshop on Formal Methods in Software Practice (FMSP '96), pages 40-48, San Diego, California, January 1996.

C. Michael Holloway. Ada 95 and Safety-Critical Software. In 14th AIAA/IEEE Digital Avionics Systems Conference, pages 504-509, November 1995. Presentation slides are available.

Victor A. Carreño. Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System. NASA Technical Memorandum 110189, NASA Langley Research Center, Hampton, Virginia, September 1995.

C. Michael Holloway, (editor). Third NASA Formal Methods Workshop 1995. NASA Conference Publication 10176, NASA Langley Research Center, Hampton, Virginia, June 1995.

Paul S. Miner. Defining the IEEE-854 Floating-Point Standard in PVS. NASA Technical Memorandum 110167, NASA Langley Research Center, Hampton, Virginia, June 1995.

Ricky W. Butler, James L. Caldwell, Victor A. Carreño, C. Michael Holloway, Paul S. Miner, and Ben L. Di Vito. NASA Langley's Research and Technology Transfer Program in Formal Methods. In Tenth Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995. A revised version is viewable here in PostScript and PDF.

C. Michael Holloway, Ben Di Vito, David Guaspari, and Michael Smith. Formal Methods: Fact vs. Fiction. In Tri-Ada '94, November 1994. Panel Summary and Position Papers.

C. Michael Holloway. Epistemology, Software Enginering, and Formal Methods. In The Role of Computers in Research and Development at Langley Research Center, pages 570-595, October 1994. NASA Conference Publication 10159.

Ricky W. Butler, Ben L. Di Vito, and C. Michael Holloway. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 3 Results). NASA Technical Memorandum 109140, NASA Langley Research Center, Hampton, Virginia, August 1994.

Ricky W. Butler. An Elementary Tutorial on Formal Specification and Verification Using PVS. NASA Technical Memorandum 108991, NASA Langley Research Center, Hampton, Virginia, September 1993. Revised in 1995.

Ricky W. Butler and Sally C. Johnson. Formal Methods For Life-Critical Software. In Computing in Aerospace 9 Conference, pages 319-329, San Diego, California, October 1993.

Paul S. Miner. Verification of Fault-Tolerant Clock Synchronization Systems. NASA Technical Paper 3349, NASA Langley Research Center, Hampton, Virginia, November 1993.

Ricky W. Butler>Ricky W. Butler and George B. Finelli. The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, 19(1):3-12, January 1993.

Ben L. Di Vito and Ricky W. Butler. Provable Transient Recovery for Frame-Based, Fault-Tolerant Computing Systems. In Real-Time Systems Symposium, Phoenix, Arizona, December 1992.

Sally C. Johnson, C. Michael Holloway, and Ricky W. Butler (editors). Second NASA Formal Methods Workshop 1992. NASA Conference Publication 10110, NASA Langley Research Center, Hampton, Virginia, November 1992.

Paul S. Miner, Peter A. Padilla, and Wilfrbsp;A. Padilla, and Wilfredo Torres. A Provably Correct Design of a Fault-Tolerant Clock Synchronization Circuit. In 11th Digital Avionics Systems Conference, pages 341-346, Seattle, Washington, October 1992.

Ben L. Di Vito and Ricky W. Butler. Formal Techniques for Synchronized Fault-Tolerant Systems. In Dependable Computing for Critical Applications 3, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1993. Also presented at 3rd IFIP Working Conference on Dependable Computing for Critical Applications, Mondello, Sicily, Italy, Sept. 14-16, 1992.

Paul S. Miner. A Verified Design of a Fault-Tolerant Clock Synchronization Circuit: Preliminary Investigations. NASA Technical Memorandum 107568, NASA Langley Research Center, Hampton, Virginia, March 1992.

Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell. High Level Design Proof of a Reliable Computing Platform. In Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, New York, 1992. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, Arizona, Feb. 18-20, 1991, pp. 124-136.

Paul S. Miner. An Extension to Schneider's General Paradigm for Fault-Tolerant Clock Synchronization. NASA Technical Memorandum 107634, NASA Langley Research Center, Hampton, Virginia, 1992.

Sally C. Johnson and Ricky W. Butler. Design For Validation. IEEE Aerospace and Electronics Systems, pages 38-43, January 1992. Also appeared in the AIAA/IEEE 10th Digital Avionics Systems Conference, Los Angeles, California, Oct. 7-11, 1991, pp. 487-492.

Ricky W. Butler and Ben L. Di Vito. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 2 Results). NASA Technical Memorandum 104196, NASA Langley Research Center, Hampton, Virginia, January 1992.

Ricky W. Butler and George B. Finelli. The Infeasibility of Experimental Quantification of Life-Critical Software Reliability. In Proceedings of the ACM SIGSOFT '91 Conference on Software for Critical Systems, pages 66-76, New Orleans, Louisiana, December 1991.na, December 1991.

Victor A. Carreño and Rob K. Angellatta. A Case Study for the Real-Time Experimental Evaluation of the VIPER Microprocessor. NASA Technical Memorandum 104098, NASA Langley Research Center, Hampton, Virginia, September 1991.

Ricky W. Butler. NASA Langley's Research Program in Formal Methods. In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, Maryland, June 1991.

Ricky W. Butler, James L. Caldwell, and Ben L. Di Vito. Design Strategy for a Formally Verified Reliable Computing Platform. In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, Maryland, June 1991.

Ricky W. Butler and Jon A. Sjogren. Formal Design Verification of Digital Circuitry. Reliability Engineering and System Safety, 32(1 and 2):67-93, 1991.

Ricky W. Butler, (editor). NASA Formal Methods Workshop 1990. NASA Conference Publication 10052, NASA Langley Research Center, Hampton, Virginia, November 1990.

Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell, II. Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 1 Results). NASA Technical Memorandum 102716, NASA Langley Research Center, Hampton, Virginia, October 1990.

Ricky W. Butler and Jon A. Sjogren. Hardware Proofs Using EHDM and the RSRE Verification Methodology. NASA Technical Memorandum 100669, NASA LangleMemorandum 100669, NASA Langley Research Center, Hampton, Virginia, December 1988.

Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Ensuring Fault-Tolerance of Phased-Locked Clocks . IEEE Transactions on Computers, Vol. C-34, p. 752-756, August 1985.

Krishna, C. M.; Shin, K. G.; and Butler, Ricky W.: Synchronization and Fault-Masking in Redundant Real-Time Systems presented by Butler at the Fourteenth International Conference on Fault-Tolerant Computing, Kissimmee, FL, June 20-22, 1984. In Proceedings, p. 152-157.

The tag identifies links that are outside the NASA domain