Laboratory for Reliable Software (LaRS)
at the Jet Propulsion Laboratory
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
Released Code
Preprocessor for C programs (gh_cpp NTR-44125) [gh_cpp.tar.gz]
Recent Publications
Contact Information
Gerard J. HolzmannMS 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 to Gerard Holzmann 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.
