Using Program Verification Tools in Teaching

“Rustan Leino chairs this session at Faculty Summit 2011, which includes the following presentations.

  • A Tour of Dafny—Rustan Leino, Microsoft Research
  • Experience with Using Dafny for Teaching an Introductory Course on Program Reasoning—Rajeev Joshi, NASA JPL
  • Teaching Using Spec# in Europe: A Experience Report from University Teaching and Various Verification Tutorials—Rosemary Monahan, National University of Ireland, Maynooth”

Speaker Details

Rustan Leino is a Principal Researcher in the RiSE group at Microsoft Research, Redmond.

Rajeev Joshi is a Senior Engineer with the Laboratory for Reliable Software at the NASA Jet Propulsion Laboratory (JPL) in Pasadena, California. His main research interests are in the study and application of formal methods to the specification and verification of software. He is currently also a member of the flight software development team for the Mars Science Laboratory Mission (MSL), serving as responsible engineer for the rover data management system, the filesystems, and spacecraft high-level communication behaviors.

Before joining JPL, he worked as a researcher at the CompaqHP Systems Research Center (SRC) in Palo Alto, California where, among other projects, he worked on the Denali superoptimizer and the theorem prover Verifun. Before starting graduate school, he also worked as a Senior Technical Associate with the Math Sciences Research Group at AT&T Bell Laboratories in Murray Hill, New Jersey. He holds a PhD in Computer Sciences from the University of Texas at Austin.

Date:
Speakers:
Rustan Leino, Rajeev Joshi, and Rosemary Monahan
Affiliation:
MSR, NASA, National University of Ireland

    • Portrait of Jeff Running

      Jeff Running

    • Portrait of Rustan Leino

      Rustan Leino

      Principal Researcher