how to do a design starting from a model that is gradually refined toward executable code

http://www.youtube.com/watch?v=fSWZWXx5ixc
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, which supports the Event-B formalism.


http://www.youtube.com/watch?v=p6D0RSo3TAY
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 correctness of the proofs. Proofs can be given in full detail, as they might be when a person first writes the proof or when the proof is intended for human understanding. Alternatively, proofs can be written with less detail, akin to the way a confident mathematician elides some details. In either case, the verification tool is satisfied only if it can fill in the missing pieces of the proof.

http://www.youtube.com/watch?v=xg4wZDJuk6o

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 refinement.

http://www.youtube.com/watch?v=P2durYFsJSA
Jason Koenig and Rustan Leino show a verification problem that makes use of functions, ghost variables, and lemmas.

http://www.youtube.com/watch?v=BLQo5d3hI4M
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

http://www.youtube.com/watch?v=kbJO-U9Wp-s

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 using the Dafny language.

http://www.youtube.com/watch?v=spcfzbisBv4

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 systematically constructed from its specifications.

K. Rustan M. Leino

http://research.microsoft.com/en-us/um/people/leino/

http://research.microsoft.com/en-us/projects/verificationcorner/

The Verification Corner is a video series on YouTube that explains different concepts of software verification.