PDF Gratis del Lenguaje de Programación C formalizado en Coq

El siguiente libro está dirigido para todas aquellas personas interesadas en aprender sobre el estándar C formalizado en Coq.

Sobre el Libro (Por el Autor)

El lenguaje de programación C fue creado por Thompson y Ritchie alrededor de 1970 como lenguaje de implementación del sistema operativo Unix.

El desarrollo de Unix demostró la eficiencia y la portabilidad de C, y luego de ese éxito, C se convirtió rápidamente en un lenguaje de programación de propósito general dominante.

Más de 40 años después de su introducción, C sigue siendo uno de los lenguajes de programación más utilizados en el mundo.

Sin embargo, a pesar de su amplio uso continuo, C también se encuentra entre los lenguajes de programación más propensos a errores en el mundo.

Como resultado de la escritura estática débil y la ausencia de controles en tiempo de ejecución, es muy fácil que los programas C tengan errores que hagan que el programa se bloquee o se comporte mal de otras formas.

Los punteros colgantes y los punteros NULL se pueden desreferenciar, se puede acceder a las matrices fuera de sus límites, etc.

Un ejemplo reciente es el error Heartbleed en la biblioteca de criptografía OpenSSL ampliamente utilizada, donde un desbordamiento de búfer permitió el acceso a datos arbitrarios, que pueden contener contraseñas.

Heartbleed no es un caso incidental donde la inseguridad de C tiene consecuencias desastrosas. Wang et al. han demostrado que la inseguridad de C es un problema grave.

En lenguajes de programación más seguros que C, es menos probable que ocurran errores como estos, pero debido a los beneficios de rendimiento, control y portabilidad de C, el uso de C y derivados de C como C++ sigue siendo generalizado.

La verificación formal es un enfoque prometedor para conservar los beneficios de rendimiento, control y portabilidad de C pero sin los peligros de su inseguridad. En la verificación formal, se utilizan métodos matemáticos para obtener el nivel más alto de garantía de la seguridad de un programa, o incluso de toda su corrección funcional.

Contenido (Temas)

Contenido
Expresiones de gratitud
Introducción
Sutilezas de C
Tipos en C
Permisos y álgebras de separación
El modelo de la memoria
CH2O núcleo C
CH2O resumen C
Lógica de separación
Formalización en Coq
Trabajo relacionado
Conclusión y trabajo futuro
Bibliografía
Sintaxis
Resumen
Samenvatting
Plan de estudios VI

Ficha Técnica

Año: 2015

Editor: Radbound University

Idioma: Inglés

Tamaño: 1655 KB

Licencia: Pendiente de revisión

Acerca de OpenLibra

OpenLibra busca reunir bajo una misma plataforma el mayor número de publicaciones libres posible. Esto implica una serie de riesgos en cuanto a los contenidos que han de asumirse y sobre los que queremos informar a nuestros usuarios.

En OpenLibra, los libros son responsabilidad exclusiva de sus autores. Esto significa que OpenLibra, no puede garantizar la validez de sus contenidos.

Te Puede Interesar

Este artículo pertenece a Facialix y está protegido por derechos de autor. Queda prohibida su reproducción total o parcial sin autorización previa del autor o titular del contenido.

Preguntas Frecuentes

¿Qué quiere decir Biblioteca Libre?

Quiere decir que todos los libros que la componen están licenciados bajo alguno de los muchos tipos de licencia libre que existen y que, por tanto, el autor da su autorización para su reproducción y redistribución.

¿Son entonces todos los libros de esta biblioteca gratis?

Sí; al menos para su versión digital. Muchos autores, además, ofrecen la versión impresa (ya sea directamente o a través del circuito comercial habitual) por la que pueden cobrar lo que estimen oportuno.

Pero algunos de los libros que hay en la Biblioteca tienen Copyright…

El copyright y las licencias libres no son excluyentes. De hecho, las segundas se basan en la legislación sobre la primera para otorgar los derechos de copia y distribución. Es por eso que toda obra bajo una licencia libre, posee un copyright que garantiza la voluntad de su autor. Lo importante es qué permite ese copyright con respecto a la obra licenciada.

Cierto; en estos casos, lo más habitual es que la editorial haya devuelto los derechos de explotación al autor. Suele ocurrir con los manuales técnicos una vez pasado un tiempo prudencial o, por ejemplo, cuando se han agotado las ediciones impresas y no se pretende una reedición. Una vez los autores vuelven a tener el control, pueden ceder su trabajo al dominio público o permitir su redistribución libre para volver a poner su obra en circulación.

Si los libros son libres y gratis, ¿puedo hacer con ellos lo que quiera? ¿Los puedo imprimir, traducir y/o vender?

No; no puedes hacer aquello que su licencia no permita. Cómo se explica en el enlace de más arriba, algunas licencias solo permiten la descarga y redistribución sin ánimo de lucro. Si por ejemplo, quieres traducir la obra y editarla de forma ordinaria, algunos autores te exigirán que pagues los derechos pertinentes.