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 Members

LaRS consists of a small core group (one person!) of formal verification experts working with a larger group of collaborators, affiliates and colleagues within JPL, and at other research centers and Universities, often collaborating in long-term projects.

LaRS members:

LaRS alumni:

  • Rajeev Joshi, PhD Univ. Texas at Austin, '04 - Sep '18.
  • Gerard J. Holzmann, PhD Delft Univ. 1979, April '03 - Dec '16.
  • Rahul Kumar, PhD Brigham Young Univ. 2008. May '14 - April '16.
  • Ed Gamble, PhD MIT, 1990, retired Aug. '14.
  • Mihaela Bobaru, PhD Univ. Toronto, 2008, April '10 - Nov '11.
  • Alex Groce, PhD CMU '05, April '05 - June '09.

Summer visitors include:

  • 2004: Kousha Etessami (U Edinburgh), Doron Peled (U. of Warwick), Peter Dillinger (Georgia Tech / NorthEastern Univ.).
  • 2005: Cheng Hu, Caltech CS.
  • 2006: John Erickson (U Texas at Austin / Intel), Jerry James (Utah State U)
  • 2007, 2008: Anna Zaks (New York University), Ru-Gang Xu (UCLA)
  • 2009: Cheng Hu (Caltech CS), Mihai Florian (Caltech CS), and Michael Van Veen (UC Davis).
  • 2010: Mihai Florian (Caltech CS)
  • 2011: Mihai Florian (Caltech CS), Eunsuk Kang (MIT CS).
  • 2012: Rachel Redberg (UC Berkeley), Spencer Reeves (UC Irvine), Richard Defrancisco (U. Stony Brook), Sasha Boulgakov (Caltech CS), Mihai Florian (Caltech CS).
  • 2013: Ioannis Filippidis (Caltech CS), Rachel Redberg (UC Berkeley), Spencer Reeves (UC Irvince), Mihai Florian (Caltech CS).
  • 2014: Ioannis Filippidis (Caltech CS).
  • 2015: Will O'Leary (Caltech CS), John Thywissen (UT Austin).
  • 2016: Frank Ortmeier, (Univ. Magdeburg, Germany), Richard DeFrancisco (U. Stony Brook).
  • 2017: Daniel Fremont (UC Berkeley)
  • 2017: Sean kauffman (Waterloo University, Canada)

Contact Information

Klaus Havelund
MS 301-450D
4800 Oak Grove Dr.
Pasadena, CA 91109-8099
(818) 354-5418

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