PROLE2009 IX Jornadas sobre Programación y Lenguajes
I Taller de Programación Funcional TPF
San Sebastián, 8-11 de septiembre de 2009
SISTEDES
Contacto  
Conferencias invitadas

K. Rustan M. Leino (Microsoft Research)Descargar conferencia

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.