Integrated program verification tools in education

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

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	de Caso, Guido, Garbervetsky, Diego, Gorín, Daniel Alejandro
Publicado:	2013
Materias:	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v43_n4_p403_DeCaso http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_00380644_v43_n4_p403_DeCaso
record_format	dspace
spelling	paper:paper_00380644_v43_n4_p403_DeCaso2023-06-08T15:02:26Z Integrated program verification tools in education de Caso, Guido Garbervetsky, Diego Gorín, Daniel Alejandro automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers 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. Copyright © 2012 John Wiley & Sons, Ltd. Copyright © 2012 John Wiley & Sons, Ltd. Fil:De Caso, G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Gorín, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2013 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v43_n4_p403_DeCaso http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
spellingShingle	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers de Caso, Guido Garbervetsky, Diego Gorín, Daniel Alejandro Integrated program verification tools in education
topic_facet	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
description	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. Copyright © 2012 John Wiley & Sons, Ltd. Copyright © 2012 John Wiley & Sons, Ltd.
author	de Caso, Guido Garbervetsky, Diego Gorín, Daniel Alejandro
author_facet	de Caso, Guido Garbervetsky, Diego Gorín, Daniel Alejandro
author_sort	de Caso, Guido
title	Integrated program verification tools in education
title_short	Integrated program verification tools in education
title_full	Integrated program verification tools in education
title_fullStr	Integrated program verification tools in education
title_full_unstemmed	Integrated program verification tools in education
title_sort	integrated program verification tools in education
publishDate	2013
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00380644_v43_n4_p403_DeCaso http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
work_keys_str_mv	AT decasoguido integratedprogramverificationtoolsineducation AT garbervetskydiego integratedprogramverificationtoolsineducation AT gorindanielalejandro integratedprogramverificationtoolsineducation
_version_	1768543361482883072

Integrated program verification tools in education

Ejemplares similares