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

Featured Projects

Toyota

Unintended Acceleration

LaRS performed the analysis for the US Department of Transportation to investigate if there could be causes for sudden unintended acceleration of Toyota vehicles triggered by software.

NSF

NSF

LaRS participated in the NSF Expeditions project "Computational Modeling and Analysis for Complex Systems (CMACS)", also known as "Model Checking and Abstract Interpretation" (MCAI 2.0).

ASE

DISM

Distributed Model Checking extends the popular Spin model checker for distributed processing on multi-core systems and multi-CPU clusters.

Rovers

FlashLite

FlashLite reliable flash file system brings rigorous software verification techniques to the development of a non-volatile file system for use on spacecraft.

Rovers

Cobra

Cobra is a powerful generic platform for the structural analysis of source code. The tool is configured to recognize C, C++, Java, Python, and Ada code, but is easily extended to accept also other languages. It is simple to write interactive queries, or to developer checker libraries for scanning code for interesting, unusual, or erroneous coding patterns. The query language supports associative arrays, variables, iteration and branching. (contact: Gerard Holzmann)

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