Program Verification in Elixir

Abstract

This project addresses the formalization and implementation of a verification system for Elixir, a dynamically typed programming language with functional programming principles. Our system is inspired by projects like Dafny and will likewise rely on a verification intermediate representation, which will be the translation target of a supported Elixir subset plus ghost verification annotations, and uses SMT solvers for its verification. The metaprogramming capabilities of Elixir through macro expressions make this language suitable for developing domain-specific languages, and allows us to provide our implementation in Elixir itself without requiring us to modify its compiler or to implement a parser. Due to the breadth of the project, we have restricted the scope to sequential code and partial correctness verification.

Este proyecto aborda la formalización e implementación de un sistema de verificación para Elixir, un lenguaje de programación funcional dinámicamente tipado. Nuestro sistema está inspirado en proyectos como Dafny y, de manera similar, se apoya en una representación intermedia de verificación, la cual será objetivo de la traducción de un subconjunto de Elixir junto con anotaciones de verificación, y utiliza resolutores SMT para su verificación. Las capacidades de metaprogramación en Elixir a través de macros hacen que este sea un lenguaje adecuado para desarrollar lenguajes específicos de dominio, y nos permiten realizar nuestra implementación en Elixir mismo, sin requerir que modifiquemos su compilador o desarrollemos un analizador sintáctico. Dada la amplitud de este proyecto, hemos restringido su alcance a código secuencial y a verificación parcial.