Ejemplos de implementación breve de interpretación abstracta

Question

Estoy tomando un curso sobre interpretación abstracta, pero no he visto ejemplos de cómo la teoría se asigna al código real.

Estoy buscando ejemplos de códigos cortos, donde preferiblemente no tendré que trabajar con un compilador completo. El análisis no tiene por qué ser útil; me gustaría ver un ejemplo en el que el análisis se deriva y luego se implementa.

¿Alguien sabe de tales ejemplos, tal vez de un curso universitario?

Answer 1

Hay MonoREIL, que viene con la herramienta de fuente abierta recientemente BinNavi.

See here es una breve introducción.

Tenga en cuenta que el contexto del marco de trabajo de MonoREIL no son los compiladores sino el análisis del código binario. Sin embargo, se ha utilizado para aplicaciones del mundo real, consulte la diapositiva 34 ff de la introducción this (que contiene más antecedentes formales).

Answer 2

No es este documento por Bertot

Structural abstract interpretation, A formal study using Coq

Eso da una implementación completa de un intérprete abstracto para un sencillo lenguaje de juguete con el asistente de pruebas Coq. Lo usé para una referencia concreta, y lo encontré útil, aunque un poco difícil, que es de esperar dado el tema. Coq es una gran pequeña pieza de software.

también me encontré en un documento Cousot:

A gentle introduction to formal verification of computer systems by abstract interpretation

detalles ásperos (pero estoy seguro de que habrá citas útiles para los detalles completos) de una implementación en Astrea, no estoy familiarizado con Astrée , por lo que no leí realmente esa sección, pero creo que cumple con sus criterios.

Si te encuentras con más, ¡por favor házmelo saber! Me gustaría especialmente ver un intérprete abstracto de prólogo.

Answer 3

AI se basa en un nombre de la teoría matemática Galois Conexión. La teoría es muy simple:

1. Resume el comportamiento del programa.
2. Realice el análisis en el nivel abstracto.

Galois connection: Relacionar el programa Actual y Abstract.

This es el mejor tutorial que he visto hasta ahora acerca de la interpretación abstracta:

Answer 4

Tal vez esta herramienta también es interesante para usted: Interproc Analyzer

Es un analizador de resumen de un lenguaje muy simple, que sin embargo ofrece análisis interprocedurales. Puede probar el análisis y obtener invariantes numéricas sobre el programa analizado. El código fuente está disponible (OCaml).

Un curso realmente minucioso y preciso, impartido por uno de los "creadores" de la Interpretación Abstracta, Patrick Cousot (ya mencionado en una de las respuestas): MIT course about Abstract Interpretation. El curso también ofrece tareas, en OCaml.