|
|
|
Registro 1 de 2, Base de información BIBCYT |
|
|
|
 Información de existencia
|
|
Resumen
This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
|
|
|
|
Registro 2 de 2, Base de información BIBCYT |
|
|
|
 Ejemplares
|
Idioma: 
Español
Descriptor Temático:
COMUNICACION,
CONFERENCIA INTELIGENCIA ARTIFICIAL Y SISTEMAS EXPERTOS 431-454,
INTERFASES PARA COMPUTADORAS |
|
Nota
TABLA DE CONTENIDO
Introducción
El lenguaje Fuente
Prueba de Equivalencia
Conclusión
Bibliografía
|
|
Descrip.
RESUMEN
En este artículo estudiamos la relación entre el llamado de procedimientos a distancia (RPC) y los lenguajes con tipajes estáticos y abstracción de tipos en particular, mostramos cómo explotar la información de tipos a fin de reducir el tiempo de transmisión de datos a través de la red. Con este próposito, desarrollamos una formalización simple que describe la generación automática de interfaces eficientes de comunicación. Terminamos nuestro estudio con una prueba de corrección que muestra la equivalencia entre la evaliuación local y la evaluación distribuida de todo programa.
|
