277
  • Writing inductive proofs about programs that operate on trees - Duration: 44 minutes.

    • 3 years ago
    • 1,923 views
    Using an extended example that flattens and reconstructs trees, Sophia Drossopoulou and Rustan Leino show how to write inductive proofs of functional programs. The verification tool checks the cor...
  • Customize your message

    Modeling, refinement, and verification - Duration: 38 minutes.

    • 3 years ago
    • 3,190 views
    In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool...
  • Customize your message

    Using ghost variables and lemmas in a program verification - Duration: 33 minutes.

    • 3 years ago
    • 798 views
    Jason Koenig and Rustan Leino show a verification problem that makes use of functions, ghost variables, and lemmas.
  • Customize your message

    Partial solutions, and comprehensions - Duration: 15 minutes.

    • 3 years ago
    • 314 views
    In this episode, Rosemary Monahan and Rustan Leino use problems specified using comprehension expressions to demonstrate how a problem can be solved using partial solutions.
  • Customize your message

    Concurrent programming in Chalice - Duration: 21 minutes.

    • 3 years ago
    • 410 views
    In this episode of Verification Corner, Peter Müller and Rustan Leino show how to specify, write, and verify a program in the Chalice language, which uses fractional permissions and implicit dynami...
  • Customize your message

    Stepwise refinement - Duration: 22 minutes.

    • 3 years ago
    • 1,722 views
    In this episode, Kuat Yessenov and Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, show how a program can be constructed by stepwise r...
  • Customize your message

    Loop termination - Duration: 21 minutes.

    • 3 years ago
    • 1,123 views
    In this episode, Rustan Leino shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it u...
  • Customize your message

    Specifications in Action - The Chunker - Duration: 14 minutes.

    • 3 years ago
    • 291 views
    In this episode, Rustan Leino writes a string "chunker" using Spec#. He gives a brief overview how one can specify and implement a program while getting the help from the Spec# verifier.
  • Customize your message

    Loop invariants - Duration: 21 minutes.

    • 3 years ago
    • 15,908 views
    In this episode, Rustan Leino talks about loop invariants. He gives a brief summary of the theoretical foundations and shows (using a problem to compute cubes) how a program can sometimes be system...
to add this to Watch Later

Add to

Loading playlists...