NASA Logo, National Aeronautics and Space Administration



  • J. Backes, S. Person, N. Rungta and O. Tkachuk. Regression Verification using Impact Summaries In International SPIN Symposium on Model Checking of Software, July 2013 (To Appear). Extended tech report
  • N. Rungta, G. Brat, W. Clancey, C. Linde, F. Raimondi, Chin S. and M. Shafto, Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems , In International Conference on Application and Theory of Automation in Command and Control Systems (ATACCS), May 2013 (To Appear)
  • J. Hunter, F. Raimondi, N. Rungta, R. Stocker, A Synergistic and Extensible Framework for Multi-Agent System Verification In International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), May 2013 (To Appear).
  • C. S. Pasareanu, W. Visser, D. Bushnell, J. Geldenhuys, P. Mehlitz, N. Rungta, Symbolic PathFinder: Integrating Symbolic Execution with Model Checking for Java bytecode analysis Automated Software Engineering Journal, 2013


  • N. Rungta, S. Person, J. Branchaud, A change impact analysis to characterize evolving program behaviors In International Conference on Software Maintenance (ICSM), Sept 2012.
  • E. Mercer, S. Person, N. Rungta, Computing and visualizing the impact of change with Java PathFinder extensions ACM SIGSOFT Software Engineering Notes 37(6): 1-5 (2012)


  • C. Pasareanu, N. Rungta, and W. Visser, Symbolic Execution with Mixed Concrete-Symbolic Solving In International Symposium on Software Testing and Analysis (ISSTA), July 2011.
  • S. Person, G. Yang, N. Rungta, and S. Khurshid, Directed Incremental Symbolic Execution In 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), June 2011.
  • D. Giannakopoulou, N. Rungta, M. Feary, Automated test case generation for an autopilot requirement prototype IEEE International Conference on Systems, Man, and Cybernetics (SMC) 2011.
  • T. Fischer, E. Mercer, and N. Rungta,   Symbolically Modeling Concurrent MCAPI Executions In 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming, San Antonio, Texas, February 2011.
  • S. Wesonga, Eric G. Mercer, N. Rungta, Guided test visualization: Making sense of errors in concurrent programs The Java PathFinder Workshop, ASE 2011.


  • C. Pasareanu and N. Rungta, Symbolic PathFinder: Symbolic Execution of Java Bytecode, Automated Software Engineering, Tool Demo, Antwerp, Beligum, October 2010
  • N. Rungta and E. Mercer, Slicing and Dicing Bugs in Concurrent programs, New Ideas and Emerging Results Track, International Conference on Software Engineering (ICSE), Cape Town, SA, May 2010.






MS Thesis

Technical Reports

Other Reports

  • N. Rungta and E. G. Mercer, Improving error discovery in guided search model checking, Prepared for BYUs Journal of Undergraduate Research (JUG), Physical and Math Sciences, 2004.


Conference Presentations

  • Clash of the Titans: Tools and Techniques for Hunting Bugs in Concurrent Programs. Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD VII), Chicago, US, July 2009.
  • Guided model checking for programs with polymorphism. ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), Savannah, January 2009.
  • Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs. Formal Methods in Computer Aided Design, Austin, US, November 2007.
  • An Improved Distance Heuristic Function for Directed Software Model Checking. Formal Methods in Computer Aided Design, San Jose, US, November 2006.
  • A Context-sensitive Structural Heuristic for Guided Search Model Checking. 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, CA, US, November 2005.

Workshop Presentations

  • Hardness in Explicit State Software Model Checking Benchmarks. Third Utah Regional Verification Workshop, Utah State University, Logan, Utah, August 2007.
  • Guided Model Checking. Second Utah Regional Verification Workshop, Brigham Young University, Provo, Utah, May 2005.

Other presentations

  • Guided Testing using Abstraction-Guided Symbolic Execution. NASA Ames Research Center, Moffet Field, California, USA. June 2009.
  • Abstraction-Guided Symbolic Execution. Microsoft Research, Redmond, Feb 2009.
  • Verifying Embedded Systems using Guided Model Checking. BYU-Nokia Seminar, Nokia Research Center, Dallas, Texas, March 2006.
  • Combining Dynamic Information with Static Analysis in Structural Heuristics. National Aeronautical and Space Administration (NASA) Ames Research Center, Moffett Field, California, USA, March 2005.
  • 19th, 20th, 21st, and 22nd Annual Spring Research Conference, College of Physical and Mathematical Science, Brigham Young University. Best presenter award for years: 2005, 2006, 2007, and 2008.



MS 269 - 1

Bldg 269 Room 230
NASA Ames Research Center
Moffett Field CA 94035

neha.s.rungta "at"

Links :

+ Brigham Young University
+ BYU CS Department
+ Blog

+ NASA Ames
+ TI Home Page
+ RSE Homepage
+ NASA Home Page

First Gov logo
NASA Logo -