NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

links
  home > team > civil servants > bld

Benedetto L. Di Vito

Selected Publications

  1. Ben L. Di Vito. Deductive Evaluation: Formal Code Analysis with Low User Burden. In FormaliSE'16, FME Workshop on Formal Methods in Software Engineering, ACM, Austin, TX, May 2016.
  2. Ben Di Vito. Formal Methods. Chapter 43 in the Digital Avionics Handbook, Third Edition. CRC Press, September 2014, ISBN 9781439868614.
  3. Eric Cooper, Benedetto Di Vito, Stephen Jacklin and Paul Miner. Baseline Assessment and Prioritization Framework for IVHM Integrity Assurance Enabling Capabilities. NASA Technical Memorandum NASA/TM-2009-215764, NASA Langley Research Center, Hampton, VA, September 2009.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. Ben L. Di Vito. Strategy-Enhanced Interactive Proving and Arithmetic Simplification for PVS. In Proceedings of STRATA 2003, First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, NASA/CP-2003-212448, Rome, Italy, September 2003.
  10. Ben L. Di Vito. A PVS Prover Strategy Package for Common Manipulations. NASA Technical Memorandum NASA/TM-2002-211647, NASA Langley Research Center, Hampton, VA, April 2002.
  11. Ben L. Di Vito. High-Automation Proofs for Properties of Requirements Models. Software Tools for Technology Transfer, 3(1), September 2000.
  12. G. Lüttgen, C. Muñoz, R. Butler, B. Di Vito, and P. Miner. Towards a Customizable PVS. ICASE Report 2000-4, NASA Report NASA/CR-2000-209851, ICASE and NASA Langley Research Center, Hampton, VA, January 2000.
  13. 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.
  14. Ben L. Di Vito. A Formal Model of Partitioning for Integrated Modular Avionics. NASA Contractor Report NASA/CR-1998-208703, NASA Langley Research Center, Hampton, VA, August 1998.
  15. Judith Crow and Ben Di Vito. Formalizing Space Shuttle Software Requirements: Four Case Studies. ACM Transactions on Software Engineering and Methodology, 7(3), July 1998.
  16. Ben L. Di Vito and Larry W. Roberts. 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, VA, August 1996.
  17. Ben L. Di Vito. Formalizing New Navigation Requirements for NASA's Space Shuttle. In Proceedings of Formal Methods Europe (FME '96), Oxford, England, March 1996. Lecture Notes in Computer Science, 1051, Springer.
  18. Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle Software Requirements. In Proceedings of Workshop on Formal Methods in Software Practice (FMSP '96), San Diego, CA, January 1996.
  19. R. Butler, J. Caldwell, V. Carreño, C. M. Holloway, P. Miner and B. Di Vito. NASA Langley's Research and Technology Transfer Program in Formal Methods. In Proceedings of COMPASS '95, Tenth Annual Conference on Computer Assurance, NIST, Gaithersburg, MD, June 1995.
  20. R. Butler, B. Di Vito and C. M. Holloway. Formal Design and Verification of a Reliable Computing Platform for Real-Time Control (Phase 3 Results). NASA Technical Memorandum 109140, August 1994.
  21. Ben L. Di Vito and Ricky W. Butler. Provable Transient Recovery for Frame-Based, Fault-Tolerant Computing Systems. In Proceedings of 13th IEEE Real-Time Systems Symposium, Phoenix, AZ, December 1992.
  22. Ben L. Di Vito and Ricky W. Butler. Formal Techniques for Synchronized Fault-Tolerant Systems. In Proceedings of Third International Working Conference on Dependable Computing for Critical Applications, Mondello, Sicily, Italy, September 1992.
  23. 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, January 1992.
  24. R. Butler, J. Caldwell and B. Di Vito. Design Strategy for a Formally Verified Reliable Computing Platform. In Proceedings of COMPASS '91, 6th Annual Conference on Computer Assurance, NIST, Gaithersburg, MD, June 1991.
  25. B. Di Vito, R. Butler and J. Caldwell. High Level Design Proof of a Reliable Computing Platform. In Proceedings of 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, AZ, February 1991.
  26. B. Di Vito, R. Butler and J. Caldwell. Formal Design and Verification of a Reliable Computing Platform for Real-Time Control. NASA Technical Memorandum 102716, October 1990.
  27. J. Caldwell, R. Butler and B. Di Vito. Hierarchical Approach to Specification and Verification of Fault-Tolerant Operating Systems. In Proceedings of Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA, July 1990.

External Activities

  • Program committee member for NASA Formal Methods Symposium (NFM) for years 2009 through 2015. Also, steering committee member.
  • Program committee member for LFM 2008, the NASA Langley Formal Methods Workshop, held 30 April through 2 May 2008 in Newport News, Virginia.
  • Presenter at NA-MKM 2004, Second North American Workshop on Mathematical Knowledge Management, Phoenix, AZ, January 2004.
  • Co-organizer and program committee member for STRATA 2003, First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, Rome, Italy, September 2003.
  • Program committee member for FME 2002, Formal Methods Europe symposium, Copenhagen, Denmark, 22-24 July 2002.
  • Program committee chair for Lfm2000, the NASA Langley Formal Methods Workshop, held 13-15 June 2000 in Williamsburg, Virginia.
  • Panelist at HASE '99, Fourth IEEE International Symposium on High Assurance Systems Engineering, Washington, DC, November 1999.
  • Member of RTCA standards committee SC-182, charged with developing the Minimum Operational Performance Standards (MOPS) for the Avionics Computer Resource (ACR) concept.
  • Program committee member for DCCA-7, the 7th IFIP Conference on Dependable Computing for Critical Applications, San Jose, CA, January 1999.
  • Program committee member and panelist for FMSP '98, Second Workshop on Formal Methods in Software Practice, Clearwater Beach, FL, March 1998.
  • Panelist at RE '97, Third IEEE International Symposium on Requirements Engineering, Annapolis, MD, January 1997.
  • Presenter and program committee member for Lfm97, the 4th NASA Langley Formal Methods Workshop, Hampton, VA, September 1997.
  • Presenter and panelist at 3rd NASA Langley Formal Methods Workshop, Hampton, VA, May 1995.
  • Participant at the Workshop on High Assurance Computing, Washington, DC, February 1995.
  • Panelist at TRI-Ada '94 Conference, Baltimore, MD, November 1994.

 

   
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ben L. Di Vito
larc privacy statement
last modified: 15 January 2016