Artículo:
A Generic Intermediate Representation for Verification Condition Generation, Work in Progress

Fecha

2015-09-15

Editor

Sistedes

Publicado en

Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015)

Licencia

Resumen

As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.

Descripción

Acerca de Montenegro, Manuel

Palabras clave

Intermediate Representation, Program Transformation, Verification Conditions, Verification Platforms
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX