NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


NFM 2013 - Keynote Speakers

  Alex Aiken, Stanford University
  Using Learning Techniques in Invariant Inference
  aiken image Dr. Alex Aiken received his Bachelors degree in Computer Science and Music from Bowling Green State University in 1983 and his Ph.D. from Cornell University in 1988. Alex was a Research Staff Member at the IBM Almaden Research Center (1988-1993) and a Professor in the EECS department at UC Berkeley (1993-2003) before joining the Stanford faculty in 2003. He is an ACM Fellow, a recipient of Phi Beta Kappa's Teaching Award, and a former National Young Investigator.
  John Rusby, SRI International
  The Challenge of High-Assurance Software
  John image Dr. John Rushby is a Program Director and SRI Fellow with the Computer Science Laboratory of SRI International in Menlo Park California, where he leads its research program in formal methods and dependable systems. He joined SRI in 1983 and served as director of its Computer Science Laboratory from 1986 to 1990. Prior to that, he held academic positions at the Universities of Manchester and Newcastle upon Tyne in England. He received BSc and PhD degrees in computing science from the University of Newcastle upon Tyne in 1971 and 1977, respectively. His research interests center on the use of formal methods for problems in the design and assurance of safe, secure, and dependable systems.
  Ken McMillan, Microsoft Research
  The Importance of Generalization in Automated Proof
  mcmillan image Dr. Ken McMillan did his Ph.D. with Turing award winner Ed Clarke at CMU, graduating in 1992. His thesis was on a technique called Symbolic Model Checking and he developed a model checker called SMV. He went on to do research at Bell Labs, Cadence Berkeley Labs, and now (as of 2010) Microsoft Research. At Cadence, he further developed SMV, incorporating methods of compositionality and abstraction to break large verification problems down into small ones in a tool called Cadence SMV. His work on Craig interpolation allows the use of logical proofs as a basis for relevance, and is used as the foundation of formal verification tools for hardware and software.


NFM 2013 - Invited Speakers

  Rajeev Joshi, Jet Propulsion Laboratory
  Managing data for Curiosity, Fun and Profit
  rajeev image Dr. Rajeev Joshi is a Senior Engineer at the NASA Jet Propulsion Laboratory in Pasadena, CA, working with the Lab for Reliable Software (LaRS). Dr. Joshi received his B.Tech in Computer Sciences from the Indian Institute of Technology, Bombay. He then worked for two years at AT&T's Bell Laboratories in Murray Hill, NJ, before starting graduate school at the University of Texas at Austin. After receiving his M.S. and PhD in Computer Sciences from UT-Austin, he joined the Compaq/HP Systems Research Center (SRC) in Palo Alto, CA, where he worked for four years before joining JPL in October 2003. His interests are in the application of formal methods to achieve improvements in software reliability and mission operations.

Michael DeWalt: Certification challenges when using formal methods, including needs and issues
This talk has been cancelled due to restrictions on government employee travel.

First Gov logo
NASA Logo - nasa.gov