RT Generic
T1 Program Verification in Elixir
T2 Verificación de programas en Elixir
A1 Enríquez Ballester, Adrián
AB 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 Elixirsubset 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 partialcorrectness verification.
AB 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 sistemaestá 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 deElixir 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 permitenrealizar 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.
YR 2022
FD 2022-07-12
LK https://hdl.handle.net/20.500.14352/73938
UL https://hdl.handle.net/20.500.14352/73938
LA eng
NO Trabajo de Fin de Máster en Métodos Formales en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y computación, Curso 2021-2022.
DS Docta Complutense
RD 9 abr 2025