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 reviewed: 30 July 2014 by Guy Power.


Publications below are categorized by year in reverse chronological order from 2013 through 2005.

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

=====================================================

RSE PUBLICATIONS

=====================================================

Brian Tietz, In Won Park, Thomas Flemons, Adrian Agogino, Roger Quinn, "Design and Control of Modular Spine-Like Tensegrity Structures," The Sixth World Conference on Structural Control and Monitoring (6WCSCM); Barcelona, Spain; 08 July 2014
[paper (PDF, 4MB)]

Jonathan Bruce, Andrew Sabelhaus, Yangxin Chen, Dizhou Lu, Kyle Morse, Sophie Milam, Ken Caluwaerts, Adrian Agogino, Vytas SunSpiral , "SUPERball: Exploring Tensegrities for Planetary Probes," 12th International Symposium on Artificial Intelligence, Robotics and Automation in Space - i-SAIRAS 2014; Montreal, Canada; 17 June 2014
[paper (PDF, 2.4MB)]

Neha Rungta, Oksana Tkachuk, Jason Biatek, Michael Whalen, Joseph Castle, Karen Gundy-Burlet, "Helping System Engineers Bridge the Peaks," Fourth International Workshop on the Twin Peaks of Requirements and Architecture; Hyderabad, India; 01 June 2014
[paper (PDF, 262KB)]

Neha Rungta, Suzette Person, Guowei Yang, Sarfraz Khurshid, "Property Differencing for Incremental Checking," 36th ICSE 2014; Hyderabad, India; 30 May 2014
[paper (PDF, 393KB)]

Neha Rungta, Franco Raimondi, Giuseppe Primero , "Model Checking Degrees of Belief in a System of Agents," AAMAS 2014; Paris, France; 5 May 2014
[paper (PDF, 365KB)]

Johann Schumann, Stefan-Alexander Schnieder, "Automated Testcase Generation for Numerical Support Functions in Embedded Systems," NASA Formal Methods 2014; Houston, TX; 8 April 2014
[paper (PDF, 274KB)]

Corina Pasareanu, Quoc-Sang Phan, Pasquale Malacaria, "Concurrent Bounded Model Checking," TACAS 2014; Grenoble, France; 5 April 2014
[paper (PDF, 262KB)]

Joseph Krall, Tim Menzies, Misty Davies, "Learning the Task Management Space of an Aircraft Approach Model," Modeling in Human-Machine Systems: Challenges for Formal Verification; Palo Alto, CA; 24 March 2014
[paper (PDF, 246KB)]

David Aspinall, Ewen Denney, Christoph Lueth, "A Semantic Basis for Proof Queries and Transformations," 19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19); Stellenbosch, South Africa; 15 December 2013
[paper (PDF, 377KB)]

Nastaran Shafiei, Peter Mehlitz, "Extending JPF to Verify Distributed Systems," The Java PathFinder Workshop; Palo Alto, CA; 12 November 2013
[paper (PDF, 205 KB)]

Matteo Ceccarello, Oksana Tkachuk, "Automated Generation of Model Classes for Java PathFinder," The Java PathFinder Workshop; Palo Alto, CA; 12 November 2013
[paper (PDF, 205 KB)]

Neha Rungta, Eric Noonan, Eric Mercer, "Vector-Clock Based Partial Order Reduction for JPF," The Java PathFinder Workshop; Palo Alto, CA; 12 November 2013
[paper (PDF, 160 KB)]

Neha Rungta, Suzette Person, "Invariant Discovery Guided By Symbolic Execution," The Java PathFinder Workshop; Palo Alto, CA; 12 November 2013
[paper (PDF, 172 KB)]

Neha Rungta, Suzette Person, Butler Hine, Eric Mercer, "Towards a Lazier Symbolic Pathfinder," The Java PathFinder Workshop; Palo Alto, CA; 12 November 2013
[paper (PDF, 250 KB)]

Neha Rungta, Suzette Person, Baishakhi Ray, Miryung Kim, "Detecting and Characterizing Semantic Inconsistencies in Ported Code," 28th IEEE/ACM International Conference on Automated Software Engineering; Palo Alto, CA; 11 November 2013
[paper (PDF, 365 KB)]

Ewen Denney, Ganeshmadhav Pai, "A Formal Basis for Safety Case Patterns," SafeComp2013; Toulouse, France; 9 November 2013
[paper (PDF, 643KB)]

Ewen Denney, Ganeshmadhav Pai, "Evidence Arguments for Using Formal Methods in Software Certification," International Workshop on Software Certification 2013; Pasadena, CA; 7 November 2013
[paper (PDF, 1.4MB)]

Johann Schumann, Kristin Rozier, Thomas Reinbacher, Ole Mengshoel, Timmy Mbaya , "Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems," Prognostics and System Health Management Conference; New Orleans, LA; 16 October 2013
[paper (PDF, 2.5MB)]

Tom Pressburger, Brian Hoelscher, Rodney Martin, Sricharan Kumar, "Simple Sensitivity Analysis for Orion GNC," AIAA Guidance, Navigation and Control Conference; Boston, MA; 18 August 2013
[paper (PDF, 496KB)]

Yuning He, Misty Davies, "Validating an Air Traffic Management Concept of Operation Using Statistical Modeling," AIAA Modeling and Simulation Technologies; Boston, MA; 3 August 2013
[paper (PDF, 1.5MB)]

Antonio Filieri, Corina Pasareanu, Willem Visser, "Reliability Analysis in Symbolic Pathfinder," International Conference on Software Engineering (ICSE); San Francisco, CA; 18 May 2013
[paper (PDF, 254KB)]

Ewen Denney, Ganeshmadhav Pai, Iain Whiteside, "Hierachical Safety Cases," 5th NASA Formal Methods Symposium; 14 May 2013
[paper (PDF, 322KB)]

Guowei Yang, Sarfraz Khurshid, Corina Pasareanu, "Memoise: A Tool for Memoized Symbolic Execution," 35th International Conference on Software engineering (ICSE 2013); San Francisco, CA; 8 May 2013
[paper (PDF, 176KB)]

Daniel Balasubramanian, Corina Pasareanu, Gabor Karsai, Michael Lowry, "Polyglot: Systematic Analysis for Multiple Statechart Formalisms," 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS); Rome, Italy; 16 March 2013
[paper (PDF, 573KB)]

Ewen Denney, Iain Whiteside, "Hierachical Safety Cases," NASA STI Report Series: TM-2013-216481; 14 February 2013
[Techinal Memorandum (PDF, 1.6MB)]

Karen Gundy-Burlet, "Validation and Verification of LADEE Models and Software," AIAA 51st Aerospace Sciences Meeting; Grapevine, TX; 07 January 2013
[paper (PDF, 315KB)]

Matt Knudson, Kagan Turner, "Dynamic Partnership Formation for Multi-Rover Coordination," Advances in Complex Systems; World Scientific Publishing, January 2013
[journal chapter (PDF, 2.7MB)]

Kagan Turner, Matt Knudson, "Efficient State Spaces and Policy Transfer for Robot Navigation," Advanced Robotics; iConcept Press, January 2013
[book chapter (PDF, 2.2MB)]

Eric Mercer, Suzette Person, Neha Rungta , "Computing and Visualizing the Impact of Change with Java PathFinder Extensions," JPF Workshop at FSE-20; Cary, NC; 9 November 2012.
[paper (PDF, 557KB)]

Artem Khyzha, Pavel Parizek, Corina Pasareanu, "Symbolic Quantitative Information Flow," JPF Workshop at FSE-20; Cary, NC; 9 November 2012.
[paper (PDF, 266KB)]

Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk, Corina Pasareanu, "Abstract Pathfinder," JPF Workshop at FSE-20; Cary, NC; 9 November 2012.
[paper (PDF, 145KB)]

Nariman Mirzaei, Sam Malek, Corina Pasareanu, Naeem Esfahani, Riyadh Mahmood , "Testing Android Apps Through Symbolic Execution," JPF Workshop at FSE-20; Cary, NC; 9 November 2012.
[paper (PDF, 145KB)]

Neha Rungta, Suzette Person, Joshua Branchaud, "A Change-Impact Analysis to Characterize Evolving Program Behaviors," Complex Aerospace Systems Exchange; 28th IEEE International Conference on Software Maintenance 2012; Riva del Garda, Trento, Italy; 29 September 2012.
[paper (PDF, 297KB)]

Ewen Denney, Ganesh Pai, and Joe Pohl, "AdvoCATE: An Assurance Case Automation Toolset," Proceedings of the Workshop on Next Generation of System Assurance Approaches for Safety Critical Systems (SASSUR); Magdeburg, Germany; 12 September 2012.
[paper (PDF, 1.1MB)]

Ewen Denney, Ganesh Pai, "A Lightweight Methodology for Safety Case Assembly," Proceedings of the 31st International Conference on Computer Safety, Reliability and Security (SafeComp '12); Magdeburg, Germany; 12 September 2012.
[paper (PDF, 293KB)]

Dimitra Giannakopoulou, Zvonimir Rakamaric, Vishwanath Raman, "Symbolic Learning of Component Interfaces," Static Analysis - 19th International Symposium, SAS 2012; Deauville, France; 11 September 2012.
[paper (PDF, 402KB)]

Misty Davies, "Assurance of Software-Intensive Flight Critical Systems: A plan for enabling validation & verification in NextGen," Complex Aerospace Systems Exchange; Pasadena, CA, 11 September 2012.
[paper (PDF, 8.1MB)]

Ewen Denney, Ganeshmadhav Pai, "Data Artifacts for Airworthiness of the Swift UAS," Oral or Visual Presentation: NAS Annual Meeting 2012; NASA Ames Research Center, Moffett Field, CA; 1 August 2012.
[PowerPoint Slides (PDF, 3.9MB)]

Ewen Denney, Ganeshmadhav Pai, "Safety Data and Risk Analysis Methods," Oral or Visual Presentation: NAS Annual Meeting 2012; NASA Ames Research Center, Moffett Field, CA; 1 August 2012.
[PowerPoint Slides (PDF, 218KB)]

Ewen Denney, Ganesh Pai, Josef Pohl, "Heterogeneous Aviation Safety Cases: Integrating the Formal and the Non-formal," 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, 2012; Paris, France; 18 July 2012.
[paper (PDF, 15.8KB)]

Matt Knudson, Kagan Turner, "Policy Transfer in Mobile Robots using Neuro-Evolutionary Navigation," Genetic and Evolutionary Computation Conference (GECCO)-2012; Philadelphia, PA; 7 July 2012.
[paper (PDF, 210KB)]

Adrian Agogino, Chris Holmes Parker, Kagan Tumer, "Evolving Distributed Resource Sharing for CubeSat Constellations," Genetic and Evolutionary Algorithms Conference; Philadelphia, PA, 7 July 2012.
[paper (PDF, 273KB)]

Adrian Agogino, Chris Holmes Parker, Kagan Tumer, "Evolving Large Scale UAV Communication System," Genetic and Evolutionary Algorithms Conference; Philadelphia, PA, 7 July 2012.
[paper (PDF, 1.2MB)]

Arnaud Venet, " The Gauge Domain: Scalable Analysis of Linear Inequality Invariants," Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA, 7 July 2012; Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012.
[paper (PDF, 345KB)]

Stephen Jacklin, "Certification of Safety-Critical Software Under DO-178C and DO278A," AIAA Infotech@aerospace - 2012, Garden Grove, CA, 19-21 June 2012.
[paper (PDF, 299KB)]

Corina Pasareanu, Anvesh Komuravelli, Edmund Clarke, "Assume-Guarantee Abstraction Refinement for Probabilistic Systems," Computer Aided Verification (CAV) 2012, Berkely, CA, 07 July 2012.
[paper (PDF, 244KB)]

Corina Pasareanu, Anvesh Komuravelli, Edmund Clarke, "Learning Probabilistic Systems from Tree Samples," Logic in Computer Science (LICS 2012), Dubrovnik, Croatia, 25 June 2012.
[paper (PDF, 215KB)]

Ewen Denney, Ganesh Pai, Ibrahim Habli, "Perspectives on Software Safety Case Development for Unmanned Aircraft," 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012), Boston, MA, 25 June 2012.
[paper (PDF, 244KB)]

Ewen Denney, Corey Ippolito, Ritchie Lee and Ganesh J. Pai, "An Integrated Safety and Systems Engineering Methodology for Small Unmanned Aircraft Systems," AIAA Infotech @ Aerospace (I@A) Conference. AIAA 2012-2572, Garden Grove, CA, 19~21 June 2012.
[paper (PDF, 1.1MB)]

Andre Goforth, "Certification of COTS Software for NASA Human Rated Flight Systems," Info Tech 2012, Garden Grove, CA, 18 June 2012.
[paper (PDF, 331KB)]

Sarah Thompson, "TUBES," Robust Software Engineering Group, NASA Ames Research Center, CA, 6 June 2012.
[Video Program Transcript (PDF, 47.5KB)]

Corina Pasareanu, Guowei Yang, Sarfraz Khurshid, "Memoized Symbolic Execution," 34th Intl Conference on Software Engineering (ICSE 2012); Zurich Switzerland; 2 June 2012
[paper (PDF, 475KB)]

Guillaume Brat, "Modeling Multiple Human-Automation Distributed Systems using Network-form Games," FormaIH, London, England, 18 May 2012.
[paper (PDF, 184KB)]

Milos Gligoric, Peter C. Mehlitz, Darko Marinov, "X10X: Model Checking a New Programming Language with an "Old" Model Checker," 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation Montreal, Quebec, Canada, 17~21 April 2012.
[paper (PDF, 136KB)]

Corina Pasareanu, "Statechart Analysis with Symbolic PathFinder," 4th Workshop on Contraints in Software Testing Verification, and Analysis; Montreal Canada; 21 April 2012
[paper (PDF, 238KB)]

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

David Aspinall, Ewen Denney, and Christoph Lüth, "Querying Proofs," 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2012), Mérida, Venezuela, March 2012.
[paper (PDF, 226KB)]

Corina Pasareanu, Guowei Yang, Sarfraz Khurshid, "Memoized Symbolic Execution," 34th Intl Conference on Software Engineering (ICSE 2012); Zurich Switzerland; 6 February 2012
[paper (PDF, 819KB)]

Mateus Borges, Marcelo d'Amorim, Saswat Anand, David H. Bushnell, Corina S. Pasareanu, "Symbolic Execution with Interval Solving and Meta-heuristic Search," 5th IEEE Fifth International Conference on Software Testing, Verification and Validation, Montreal, QC, Canada, April 17-21, 2012.
[paper (PDF, 446KB)]

Corina Pasareanu, Guowei Yang, Sarfraz Khurshid, "Memoized Symbolic Execution," 34th Intl Conference on Software Engineering (ICSE 2012); Zurich Switzerland; 6 February 2012
[paper (PDF, 819KB)]

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)]

Krishnendu Chatterjee, Vishwanath Raman, "Synthesizing Protocols for Digital Contract Signing," Verification, Model Checking, and Abstract Interpretation - 13th International Conference (VMCAI 2012), Philadelphia, PA, 22-24 January 2012.
[paper (PDF, 446KB)]

Corina Pasareanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, "Symbolic PathFinder: Integrating Symbolic Execution with Model Checking for Java Bytecode Analysis," Automated Software Engineering; Springer Verlag; Montreal Canada; 6 January 2012
[book chapter (PDF, 819KB)]

Adrian Agogino, Kagan Tumer, "A Multiagent Approach to Managing Air Traffic Flow," Autonomous Agents and Multi-Agent Systems, Volume 24, No. 1, Springer, 1 January 2012.
[journal article (External Link)]

Peter C. Mehlitz, Oksana Tkachuk, Mateusz Ujma, "JPF-AWT: Model checking GUI applications," 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, 6-10 November 2011.
[paper (PDF, 486KB)]

Ewen Denney, Ganesh Pai, Ibrahim Habli, "Perspectives on Software Safety Case Development for Unmanned Aircraft," 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012), Boston, MA, 11 October 2011.
[paper (PDF, 244KB)]

Sébastien Combéfis, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary, "A Formal Framework for Design Analysis of Human-Machine Interaction," 2011 IEEE International Conference on Systems, Man and Cybernetics, Anchorage, AK, 9 October 2011.
[paper (PDF, 373KB)]

Dimitra Giannakopoulou, Neha Rungta, Michael Feary, "Automated test case generation for an autopilot requirement prototype," 2011 IEEE International Conference on Systems, Man and Cybernetics, Anchorage, AK, 9 October 2011.
[paper (PDF, 190KB)]

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)]

Christian Roth, Matt Knudson, Kagan Turner, "Agent Fitness Functions for Evolving Coordinated Sensor Networks," Genetic and Evolutionary Computation Conference (GECCO)-2011; Dublin, Ireland; 12 July 2011.
[paper (PDF, 865KB)]

Ewen Denney, Ganesh Pai, Josef Pohl, "Automating the Generation of Heterogeneous Aviation Safety Cases," Technical Report No. NASA/CR-2011-215981; NASA Ames Research Center, CA; August 2011.
[technical report (PDF, 15.8MB)]

Corina Pasareanu, Neha Rungta, and Willem Visser, "Symbolic Execution with Mixed Concrete-Symbolic Solving," In International Symposium on Software Testing and Analysis (ISSTA); Toronto, Canada; 17~21 July 2011.
[paper (PDF, 231KB)]

Kristin Rozier, Moshe Vardi, "A Multi-encoding Approach for LTL Symbolic Satisfiability Checking," 17th International Symposium on Formal Methods, Limerick, Ireland, 20~24 June 2011. volume 6664 of Lecture Notes in Computer Science (LNCS), pages 417--431
[paper (PDF, 2.5MB)]

Dimitra Giannakopoulou, Corina S. Pasareanu, "Context Synthesis," SFM-11:CONNECT , 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Connectors for Eternal Networked Software Systems, Bertinoro, Italy, 13 June 2011.
[paper (PDF, 1MB)]

Knudson, M. and Tumer, K., "Adaptive Navigation for Autonomous Robots'', Robotics and Autonomous Systems, Volume 59, Issue 6, Pages 410-420, June 2011
[journal chapter]

Daniel Balasubramanian, Gábor Pap, Harmon Nine, Gabor Karsai, Michael R. Lowry, Corina S. Pasareanu, Thomas Pressburger, "Rapid property specification and checking for model-based formalisms," 22nd IEEE International Symposium on Rapid System Prototyping (RSP 2011), Karlsruhe, Germany, 24~27 May 2011.
[paper (PDF, 2MB)]

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)]

Domenico Bianculli, Dimitra Giannakopoulou, Corina S. Pasareanu, "Interface Decomposition for Service Compositions," 33rd International Conference on Software Engineering (ICSE 2011), Honolulu, HI, 21 May 2011.
[paper (PDF, 709)]

Kristin Rozier, "Linear Temporal Logic Symbolic Model Checking," Computer Science Review, Vol. 5, Issue 2; pp. 163-203, Elsevier, May 2011.
[paper (PDF, 3.9MB)]

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)]

Gregory Gay, Tim Menzies, Misty Davies, Karen Gundy-Burlet, "Automatically finding the control variables for complex system behavior," Automated Software Engineering, Volume 17, Number 4 (2010), Springer Publishing, pp. 439-468, December 2010.
[journal article (PDF, 747KB)]

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)]

Ewen Denney, Ibrahim Habli, and Ganesh Pai, "Towards Measurement of Confidence in Safety Cases," Proceedings of the 5th International Symposium on Empirical Software Engineering and Measurement (ESEM '11); Banff, Canada; 22 September 2011.
[paper (PDF, 200KB)]

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

Nurlida Basir, Ewen Denney and Bernd Fischer, "Deriving Safety Cases for Hierarchical Structure in Model-based Development," 29th International Conference on Computer Safety, Reliability and Security (SAFECOMP '10), Vienna, Austria, 14 September 2010.
[paper (PDF, 173KB)]

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)]

Knudson, M. and Tumer, K., "Coevolution of Heterogeneous Multi-Robot Teams,” Genetic and Evolutionary Computation Conference (GECCO); Portland OR; July 2010
[paper]

Johann Schumann, Dimitra Giannakopoulou, David Bushnell, " Formal Testing for Seperation Assurance ," Special Issue Annals of Math and Artificial Intelligence, Volume 63, Number 1, September 2011; Springer Verlag, September 2011.
[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)]

Kristin Rozier, Moshe Vardi, "LTL satisfiability checking," International Journal on Software Tools for Technology Transfer (STTT),Volume 12, Issue 2, pp 123~137 Springer-Verlag, March, 2010.
[paper (PDF, 919KB)]

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)]

Knudson, M. and Tumer, K., "Neuro-Evolutionary and Policy Gradient Methods for Autonomous Navigation,'' Workshop on Autonomous and Learning Agents (ALA); Toronto Canada; May 2010
[paper]

Knudson, M. and Tumer, K., "Robot Coordination with Ad-hoc Team Formation,” Autonomous Agents and Multiagent Systems (AAMAS); Toronto Canada; May 2010
[short paper]

Sarah Thompson, Misty Davies, Karen Gundy-Burlet, "Hybrid Decompositional Verification for Discovering Failures in Adaptive Flight Control Systems," AIAA Infotech@Aerospace, Atlanta, GA, 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)]

Danny Thomas, Alexia Joiner, Wei Lin, Michale Lowry, Thomas Pressburger, "The Unique Aspects of Simulation Verification and Validation ," IEEE Aeorspace Conference 2010, Big Sky, MT, 6~10 March 2010.
[paper (PDF, 147MB)]

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,"b 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, 1.5MB)]

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

David Bushnell, "Review: Beautiful Code," "Scientific Programming" Volume 17, Number 3 ,2009.
[book review (External Site HTML, 38.4KB)]

Knudson, M. and Tumer, K., ”Coordinating Autonomous Robots for Exploration in Dynamic Environments,” Artificial Neural Networks in Engineering (ANNIE), pg. 587-594, St. Louis MO, November 2008
[conference paper]

Knudson, M. and Tumer, K., ”Neuro-Evolutionary Navigation for Resource-Limited Mobile Robots,” Artificial Neural Networks in Engineering (ANNIE), pg. 27-34, St. Louis MO, November 2008
[conference paper]

Junell, J., Knudson, M. and Tumer, K., ”Optimizing Sensor / Neuro-Controller Pairings for Effective Navigation,” Artificial Neural Networks in Engineering (ANNIE), pg. 19-26, St. Louis MO, November 2008
[conference paper]

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, Hamid Jafari, Thomas Pressburger, Ewen Denney, Wray Buntine, Bernd Fischer, "AutoBayes Program Synthesis System Users Manual," TM, 8 August 2008.
[User's 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)]

Corina Păsăreanu, Peter Mehlitz, David Bushnell, Karen Gundy-Burlet, Mike Lowry, Suzette Person, Mark Pape, "Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software," ISSTA (International Symposium on Software Testing and Analysis), Seattle, WA,” July 2008.
[paper (PDF, 907KB)]

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)]

Thomas T. Pressburger, Masoud Mansouri-Samani, Peter C. Mehlitz, Corina S. Pasareanu, John J. Penix, Guillaume P. Brat, Lawrence Z. Markosian, Owen O’Malley, Willem C. Visser, "Program Model Checking -- A Practitioner’s Guide," NASA/TM-2008-214577,” NASA Ames Research Center, Moffett Field, CA; March 2008.
[technical memorandum (PDF, 682KB)]

Matt Knudson, "Applying Hierarchical and Adaptive Control to Coordinating Autonomous Robots," M.S. Thesis, Mechanical Engineering; Oregon State University, 2008
[Thesis]

Knudson, M. and Schmitt, J., ”Mentor Graphics SystemVision Software Curriculum Integration,” American Society for Engineering Education (ASEE), Honolulu HI, June 2007
[conference paper]

Donnelly, M. and Knudson, M., ”Mini-Baja Traction Control System - Mechatronics Modeling,” SAE World Congress and Exhibition, Detroit MI, April 2006
[conference paper]

Edward Balaban, Michael D. Orosz, Tatiana Kichkaylo, Andre Goforth, Adam Sweet, Robert Neches, ”Planning to Explore: Using a Coordinated Multisource Infrastructure to Overcome Present and Future Space Flight Planning Challenges,” AAAI Spring Symposium: Distributed Plan and Schedule Management 2006: 9-16, Stanford, California, March 27-29, 2006.
[paper (PDF, 437KB)]

Gary Lindstrom, Peter C. Mehlitz, Willem Visser, "Model Checking Real Time Java Using Java PathFinder," Automated Technology for Verification and Analysis,” Lecture Notes in Computer Science, Volume 3707/2005, 444-456; Springer, 2005.
[book chapter (PDF, 229KB)]

Peter C. Mehlitz, John Penix, "Design for Verification with Dynamic Assertions," 29th Annual IEEE / NASA Software Engineering Workshop (SEW-29 2005),” Greenbelt, Maryland, 6~7 April 2005.
[workshop paper (PDF, 127KB)]

Willem Visser, Peter C. Mehlitz, "Model Checking Programs with Java PathFinder," 12th International SPIN Workshop,” San Francisco, 22-24 Aug 2005.
[workshop PowerPoint (PDF, 793KB)]

First Gov logo
NASA Logo - nasa.gov