formulog

Formulog

TL; DR: Escribir análisis de programas basados ​​en SMT (ejecutores simbólicos, verificadores de tipo de refinamiento, etc.) en un lenguaje optimizado de tipo datos.

DataSalog ha demostrado ser un lenguaje útil para implementar una gama de análisis de programas, pero los análisis que usan la resolución de SMT no se pueden escribir fácilmente en versiones tradicionales de DataSalog. Formulog se establece para llenar este vacío aumentando Datalog con formas de construir y razonar sobre las fórmulas SMT, así como una programación funcional de primer orden para facilitar la vida.

¿Por qué escribir su análisis basado en SMT en Formulog?

1. Al combinar la programación lógica, la programación funcional y la resolución de SMT, Formulog permite codificar muchos análisis declarativamente al nivel de especificación matemática (por ejemplo, reglas de inferencia), cerrar la brecha entre la especificación y la implementación, y a menudo revelando errores en la especificación!
2. Esta codificación de alto nivel hace posible que Formulog aplique optimizaciones de alto nivel a su análisis, como la paralelización automática y la evaluación dirigida por objetivos.
3. Gracias a nuestro compilador Formulog-to-Soufflé, puede generar automáticamente una versión C ++ del análisis que aprovecha algoritmos de datos y estructuras de datos altamente optimizadas.

¿Interesado? Para obtener más información, consulte los documentos de Formulog (también disponibles en el directorio de documentos), incluidos los consejos sobre cómo comenzar y la referencia del idioma. Para tener una sensación de lo que implica la construcción de un análisis no trivial basado en SMT en Formulog, consulte nuestro tutorial sobre la implementación de un verificador de tipo de refinamiento en Formulog.

Que contribuye

¡Las contribuciones a este proyecto son más bienvenidas! Abra un problema de GitHub y luego vincule una solicitud de extracción. Las solicitudes de extracción deben estar en el formato de Google Java antes de fusionarse. Para reformatear su código, ejecute mvn spotless:apply ; También puede verificar si su código es conforme (sin reformatearlo) ejecutando mvn spotless:check .

Licencias y bibliotecas de terceros

Formulog se libera bajo una licencia Apache 2.0.

Este proyecto utiliza bibliotecas de terceros. Puede generar una lista de estas bibliotecas y descargar sus licencias asociadas con este comando:

 mvn license:download-licenses

El contenido generado se puede encontrar en el directorio de target/generated-resources/ .