Qed at Large: Un estudio de ingeniería de software verificado formalmente

Título original:

Qed at Large: A Survey of Engineering of Formally Verified Software

Contenido del libro:

El desarrollo de pruebas formales de la corrección de los programas puede aumentar la fiabilidad real y percibida y facilitar una mejor comprensión de las especificaciones de los programas y sus supuestos subyacentes. Hace más de 40 años que se dispone de herramientas para este tipo de desarrollo, pero sólo recientemente se ha generalizado su uso práctico.

Los proyectos basados en la construcción de pruebas formales verificadas por máquinas están alcanzando ahora una escala sin precedentes, comparable a la de los grandes proyectos de software, lo que plantea nuevos retos en el desarrollo y mantenimiento de pruebas. A pesar de su creciente importancia, el campo de la ingeniería de pruebas rara vez se considera por derecho propio; las teorías, técnicas y herramientas relacionadas abarcan muchos campos y lugares. QED at Large cubre la cronología y la literatura de investigación relativa al desarrollo de pruebas para la verificación de programas, incluyendo teorías, lenguajes y herramientas.

Destaca los retos y avances en cada etapa de la historia y subraya los retos actuales debido a la creciente escala de los desarrollos de pruebas. Esta monografía está destinada a investigadores y estudiantes que se inician en este campo.

Ofrece al lector una visión de conjunto de los trabajos que han conducido a las técnicas actuales de verificación formal del software. En una época de creciente automatización, este campo es la base de muchos sistemas de software, por lo que también se destacan las tendencias futuras.