NASA Logo, National Aeronautics and Space Administration

Publications

Synthesis

The goal of the Program Synthesis Projects is to use techniques from artificial intelligence and formal methods to raise the level at which users program to the specification level (which describes the problem to be solved) from the code level (which describes how to solve the problem).

Verification & Validation

The goal of this project is to develop and apply automated tools, such as model checkers and static analyzers, in the verification and validation of critical software systems.

Last modified: 14 May 2012 by Guy Power.


Publications below are categorized by year in reverse chronological order from 2012 through 2008.

Publications are also listed by senior author (see staff web pages HERE)

Corina Pasareanu, Tom Pressburger, Michael Lowry, Gabor Karsai, Daniel Balasubramanian,"Integrating Statechart Components in Polyglot," 4th NASA Formal Methods 2012, Norfolk, VA, 03 April 2012.
[paper (PDF, 88.4KB)]

Misty Davies, Vishwanath Raman, Corina Pasareanu," Symbolic Execution Enhanced System Testing," Verified Software: Theories, Tools and Experiments, Philadelphia, PA, 27 January 2012.
[paper (PDF, 377KB)]

Johann Schumann,"SWHM: Tools and Techniques for Software and System Health Management," DashLink, NASA Only Website, 29 September 2011.
[paper (PDF, 12.8MB)]

Misty Davies,"Model-Based Validation Testing," Oral/Visual Presentation at FAA/JPDO/NASA, Egg Harbor, NJ, 28 September 2011.
[paper (PDF, 2.5MB)]

Misty Davies, Nathan Aguirre,"Determining the Number of Clusters In a Data Set Without Graphical Interpretation," NASA Ames Student Poster, Moffett Field, CA, 8 August 2011.
[paper (PDF, 2MB)]

Misty Davies, Corina Pasareanu, Vishwanath Raman, "Symbolic Execution Enhanced System Testing," 33rd International Conference on Software Engineering (ISCE 2011), Honolulu, HI, 21 May 2011.
[paper (PDF, 391K)]

Corina Pasareanu, Christian Cadar, Patrice Godefroid, Sarfranz Khurshid, Koushik Sen, "Symbolic Execution for Software Testing in Practice Preliminary Assessment," 33rd International Conference on Software Engineering (ICSE 2011), Honolulu, HI, 21 May 2011.
[paper (PDF, 156K)]

Neha Rungta, Topher Fischer, Eric Mercer, " Symbolically Modeling Concurrent MCAPI Executions," 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming 2011, San Antonio, TX, 28 February 2011.
[paper (PDF, 131K)]

Arnaud Venet, Michael Lowry, " Static Analysis for Software Assurance-Soundness, Scalability and Adaptiveness," Workshop on the Future of Software Engineering Research, Santa Fe, NM, 07 November 2010.
[paper (PDF, 162KB)]

Corina Pasareanu, Neha Rungta, "Symbolic Pathfinder: Symbolic Execution of Java Bytecode," 25th Intnl Conference on Automated Software Engineering, Antwerp, Belgium, 20 September 2010.
[paper (Coming Soon)]

Misty Davies, Karen Gundy-Burlet, Gregory Limes, "A Hardware Model Validation Tool for Use In Complex Space Systems," AIAA Space 2010, Pasadena, CA, 31 August 2010.
[paper (PDF, 1.5MB)]

Brian Glass, Sarah Thompson, Gale Paulsen, "Robotic Planetary Drill Tests," 10th International Symposium on Artificial Intelligence, Sapporo, Japan, 29 August 2010.
[paper (PDF, 2.6MB)]

Johann Schumann, Karen Cate, Alan Lee, " Analysis of Air Traffic Track Data with the AutoBayes Synthesis System," Computer Aided Verification (CAV 2010), Edinburgh, Scotland (UK), 23 July 2010.
[paper (PDF, 1.2MB)]

Rishabh Singh, Dimitra Giannakopoulou, Corina Pasareanu, "Learning Component Interfaces with May and Must Abstractions," Computer Aided Verification (CAV 2010), Edinburgh, Scotland (UK), 15 July 2010.
[paper (PDF, 230KB)]

Johann Schumann, Dimitra Giannakopoulou, David Bushnell, " Formal Testing for Seperation Assurance ," Special Issue Annals of Math and Artificial Intelligence, Springer Verlag, 10 June 2010.
[paper (PDF, 356KB)]

Johann Schumann, Ole Mengshoel, Adnan Darwiche, "ISWHM: Tools and Techniques for Software and System Health Management," DASH/Software Health Management TIM 2010, NASA Ames Research Center, Moffett Field, CA, 10 June 2010.
[paper (PDF, 1.2MB)]

Neha Rungta, Eric Mercer, "Slicing and Dicing Bugs in Concurrent Programs," 32nd International Conference on Software Engineering, Cape Town, South Africa, 2 May 2010.
[paper (PDF, 155KB)]

Misty Davies, Karen Gundy-Burlet, "Visualization of Global Sensitivity Analysis Results Based on a Combination of Linearly Dependent and Independent Directions," AIAA Infotech@Aerospace, Atlanta, GA, 20 April 2010.
[paper (PDF, 475KB)]

Sarah Thompson, Misty Davies, Karen Gundy-Burlet, "Compositional Verification for Discovering Failures in Adaptive Flight Control Systems ," AIAA Infotech@Aerospace, Atlanta, GA, 20 April 2010.
[paper (PDF, 471KB)]

Sarah Thompson, Misty Davies, Karen Gundy-Burlet, "Compositional Verification for Discovering Failures in Adaptive Flight Control Systems ," AIAA Infotech@Aerospace, Vienna, Austria, 20 April 2010.
[paper (PDF, 471KB)]

Nurlida Basir, Ewen Denney, Bernd Fischer, "Deriving Safety Cases for Hierachical Systems in Model-Based Development," SAFECOMP 2010, Vienna, Austria, 22 March 2010.
[paper (PDF, 214KB)]

Ewen Denney, David Aspinall, Christoph Lüth, "Tactics for Hierarchical Proof," Mathematics in Computer Science: Special Issue on Authoring, Digitalization and Management of Mathematical Knowledge, Mathematics in Computer Science:, 03 May 2010.
[paper (PDF, 344KB)]

Johann Schumann and Yan Liu (editors), "Neural Networks in High-Assurance Applications (ed)," Book Editor and Chapter: Application of Neural Networks in High Assurance Systems, Vol. 268, Springer Verlag, 01 March 2010.
[Book Cover (PDF, 5MB)]

Johann Schumann, Pramod Gupta, Yan Liu,"Application of Neural Networks in High Assurance Systems - A Survey ," Book Chapter: Application of Neural Networks in High Assurance Systems, Vol. 268, Springer Verlag, 15 February 2010.
[paper (PDF, 201KB)]

Sarah Thompson, Guillaume Brat, Arnaud Venet,"Software Model Checking of ARINC-653 Flight Code with MCP ," NASA Formal Methods Symposium (NFM 2010), Washington, D.C., 18 January 2010.
[paper (PDF, 94.4KB)]

Sarah Thompson, Guillaume Brat, Arnaud Venet,"Software Model Checking of ARINC-653 Flight Code with MCP," NASA Formal Methods Symposium (NFM 2010), Washington, D.C., 18 January 2010.
[paper (PDF, 94.4KB)]

Ewen Denney,"A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software," IEEE/ACM International Conference on Automated Software Engineering, 16 November 2009.
[paper (PDF, 2.3MB)]

Sarah Thompson, Misty Davies, Karen Gundy-Burlet,"Compositional Verification for Discovering Failures in Adaptive Flight Control Systems," AIAA Infotech, 06 November 2009.
[paper (PDF, 296KB)]

Misty Davies, Karen Gundy-Burlet,"Visualization of Global Sensitivity Analysis Results Based on a Combination of Linearly Dependent and Independent Directions," AIAA Infotech, 06 November 2009.
[paper (PDF, 475KB)]

Ewen Denney, Bernd Fischer, Nurlida Basir,"Deriving Safety Cases from Automatically Constructed Proofs," 4th IET International Conference on System Safety, 26 October 2009.
[paper (PDF, 357KB)]

Raj Thirumalainambi, Johann Schumann, Peter Berg, Anupa Bajwa,"Parameter Estimation of ERIS Model Using Monte Carlo Error," Conference on Intelligent Data Understanding (CIDU), 14 October 2009.
[paper (PDF, 6.4KB)]

Johann Schumann, Karen Tung," Data Mining of Air traffic Track Data for NGATS," Conference on Intelligent Data Understanding (CIDU), 14 October 2009.
[paper (PDF, 6.4KB)]

KiYung Ahn, Ewen Denney,"Testing First-Order Axioms in AutoCert," 7th Asian Symposium on Programming Languages and Systems (APLAS 2009) and Systems (APLAS 2009) (CIDU), 08 October 2009.
[paper (PDF, 82.7)]

Guillaume Brat, Dimitra Giannakopoulou, Michel Izygon, Emmy Alex, Lui Wang,"Model-based Verification and Validation for Procedure Authoring," Verification and validaiton of planning and scheduling systems, 20 September 2009.
[paper (PDF, 513KB)]

Guillaume Brat, Franco Raimondi, Charles Pecheur,"PDVer, a Tool to Verify PDDL Planning Domains," Verification and validation of planning and scheduling systems,, 20 September 2009.
[paper (PDF, 441KB)]

Ole Mengshoel, Johann Schumann, Knot Pipatsrisawat, Adrian Darwiche,"Software Health Management - A Short Review of Challenges and Existing Techniques" 1st International Workshop on Software Health, 21 July 2009.
[paper (PDF, 81.8KB)]

Guillaume Brat," A Formal Analysis of Requirements-Based Testing," International Symposium on Software Testing, 19 July 2009.
[paper (PDF, 238KB)]

Corina Pasareanu, Johann Schumann, Peter Mehlitz, Michael Lowry, Gabor Karsai,"Model Based Analysis and Test Generation for Flight Software," SMC-IT Conference, 19 July 2009.
[paper (PDF, 337KB)]

Ewen Denney,"The Future of Software Certification - a Roadmap," Frontiers of Automated Software Engineering, 15 July 2009.
[paper (PDF, 3.2MB)]

Ewen Denney,"Generating Code Review Documentation for Auto-Generated Mission-Critical Software," 3rd IEEE International Conference on Space Mission Challenges for Information Technology, 13 July 2009.
[paper (PDF, 3.2MB)]

Dimitra Giannakopoulou, Corina Pasareanu,"Interface Generation and Compositional Verification in JavaPathfinder," ETAPS 2009 (FASE 2009), 22 March 2009.
[paper (PDF, 3.2MB)]

Johann Schumann,"ISWHM: Tools And Techniques for Software and System Health Management," NASA Aviation Safety Meeting, 21 October 2008.
[paper (PDF, 11.5MB)]

Johann Schumann,"Tool Support for Parametric Analysis of Large Software Simulation Systems," Automated Software Engineering; Tools Workshop, 15 September 2008.
[paper (PDF, 291KB)]

Steven Jacklin,"Closing the Certification Gaps in Adaptive Flight Control Software," 2008 GNC CONFERENCE, 18 August 2008.
[paper (PDF, 302KB)]

Johann Schumann,"AutoBayes Program Synthesis System Users Manual," TM, 8 August 2008.
[Technical Manual (PDF, 1.8MBB)]

Ewen Denney,"Generating Customized Verifiers for Automatically Generated Code," Generative Programming and Component Engineering (GPCE'08), 28 July 2008.
[paper (PDF, 175KB)]

Corina Pasareanu,"A Survey of New Trends in Symbolic Execution for Software Testing and Analysis," International Journal on Software Tools for Technology Transfer, (Springer Verlag)” 07 July 2008.
[paper (PDF, 317KB)]

Mihaela Gheorghiu, Corina Pasareanu, Dimitra Giannakopoulou,"Automated Assume-Guarantee Reasoning by Abstraction Refinement," 20th International Conference on Computer Aided Verification,” 07 July 2008.
[paper (PDF, 232KB)]

Johann Schumann,"Model Based Analysis and Test Generation for Flight Software," ICSE 2009,” 16 May 2008.
[paper (PDF, 697KB)]

Karen Gundy-Burlet,"Parametric Analysis of a Hover Test Vehicle using Advanced Generation and Data Analysis," AIAA Infotech@Aerospace Conference and Exhibit,” 04 April 2008.
[paper (PDF, 691KB)]

First Gov logo
NASA Logo - nasa.gov