Artículo
Integrated program verification tools in education
Fecha de publicación:
04/2013
Editorial:
Wiley
Revista:
Software: Practice And Experience
e-ISSN:
1097-024X
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
Automated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large-scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of programs that arise in introductory programming courses. This opens exciting new opportunities in teaching the basics of reasoning about program correctness to novice students. However, for these tools to be effective, command-line-style user-interfaces need to be replaced. In this paper, we report on our experience using the verifying compiler for PEST in an introductory programming course as well as in a more advanced course on program analysis. PEST is an extremely basic programming language, but with expressive annotations capabilities and semantics amenable to verification. In particular, we comment on the crucial role played by the integration of this verifying compiler with the Eclipse integrated development environment.
Palabras clave:
Education
,
Formal Methods
,
Automated Program Verification
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(OCA CIUDAD UNIVERSITARIA)
Articulos de OFICINA DE COORDINACION ADMINISTRATIVA CIUDAD UNIVERSITARIA
Articulos de OFICINA DE COORDINACION ADMINISTRATIVA CIUDAD UNIVERSITARIA
Citación
de Caso, Guido; Garbervetsky, Diego David; Gorin, Daniel Alejadro; Integrated program verification tools in education; Wiley; Software: Practice And Experience; 43; 4; 4-2013; 403-418
Compartir
Altmétricas