K. Rustan M. Leino (Microsoft Research)

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

Título: "Understanding program verification"

Resumen: With program semantics and decision procedures, we can build automatic program verifiers. But can users understand how to use the program verifier or does that still require a PhD? In this talk, I will discuss how program and specification language features, the running of the program verifier, and the presentation of the verifier's output affect usability. I will draw from experience with different language front ends for the Boogie program verifier and will sketch a vision for an understandable, responsive, and ceaselessly analyzing verification environment.