Skip to main content
These web pages use cascading style sheet features for formatting. You may still browse the text of the site, but for best results, use a modern CSS-enabled browser.

Laboratory for Reliable Software (LaRS)
at the Jet Propulsion Laboratory

Title Image

LaRS Overview

The Laboratory for Reliable Software (LaRS) was created in 2003 and became an independent Center of Excellence at JPL in the Systems and Software Division in 2005.

The Lab's mission is to achieve long term improvements in the reliability of JPL's mission critical software systems. To do so, it pursues a research program that targets the application of both new and existing formal verification techniques to mission software. This means that a good portion of the activities of the lab are project-driven. The group members try to identify key vulnerabilities in mission software and try to find meaningful remedies for them. LaRS members collaborate also with JPL's Software Quality Initiative (SQI), Software Quality Assurance (SQA), the JPL Safety Office on software-related R&TD initiatives. LaRS members also have strong connections with colleagues at leading Universities and research labs worldwide, and specifically also with researchers at other NASA centers, such as NASA Ames Research, Kennedy Space Center, Johnson Space Center, Langley, Marshall, and Goddard.

LaRS projects can target any part of the software life-cycle, from requirements capture and analysis, to high-level and low-level software design, coding, testing, deployment and mission operations. We occassionally work directly on specific missions, but more often we take on a more generic advisory role across all projects. We seek to partner with other groups to develop, apply, and introduce improved tools and technologies into mainstream JPL software engineering practice to achieve overall improvements in software reliability.

Topics of interest include new and existing formal software testing and verification strategies for

  • requirements capture, analysis, and tracking
  • design verification
  • static source code analysis
  • logic model checking (both symbolic and explicit state methods)
  • automata based testing
  • randomized testing techniques
  • swarm based techniques (multi-core, distributed)
  • tool-support for peer code review processes
  • runtime monitoring and verification
  • software quality and reliability metrics
  • auto coding techniques
  • logic verification of AI-based planners
  • design verification of fault protection code
  • fault tolerance, fault containment, survivability
Our general approach is focused on tool-based verification methods. We research, build, improve, and apply state-of-the-art tools that harness new theory and technology that can help improve software reliability.

Released Code

Simple code counter for C programs (ncsl NTR-44124) [ncsl.tar.gz]
Preprocessor for C programs (gh_cpp NTR-44125) [gh_cpp.tar.gz]

Selected Publications

JPL Institutional Coding Standard for the C Programming Language [PDF] developed in collaboration with Grammatech, checkers for the rules in this standard are available from Grammatech and Semmle
JPL Coding Standard for Java [PDF] developed in collaboration with Semmle, checkers for the rules in this standard are available from Semmle.
Aspect-oriented monitoring of C programs [PDF] K. Havelund, E. van Wyk Proc. Sixth IARP-IEEE/RAS-EURON Joint Workshop on Technical Challenges for Dependable Robots in Human Environments, Pasadena, CA, May 17-18, 2008.
Randomized differential testing as a prelude to formal verification [PDF] A. Groce, G.J. Holzmann, R. Joshi Proc. ICSE, Minneapolis, MN. May 2007
The Design of a multi-core extension of the Spin Model Checker [PDF] G.J. Holzmann, D. Bosnacki IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674, October 2007.

Contact Information

Klaus Havelund / Rajeev Joshi
MS 301-451
4800 Oak Grove Dr.
Pasadena, CA 91109-8099
(818) 393-5937
E-mail: Firstname dot Lastname at jpl dot nasa dot gov

Employment Opportunities

Applications for positions in LaRS are welcome. Please send an e-mail with a statement of interest and a resume. We specifically seek candidates with a strong background in formal methods and software verification techniques. To be eligible for employment by JPL, candidates must be US citizens or have permanent residence in the U.S.

We also welcome applications for long- or short-term internships. Please check with us if you are interested.

+ JPL Career Launch

Internal JPL-Only Links

+ LaRS internal website