Enrique Martín

Associate Professor

Academic Coordinator of Master's in Computer Science Engineering

Facultad de Informática

Universidad Complutense de Madrid

About

Research

Research projects:

Funding agencies:
  • : European Union
  • : Ministries of the Kingdom of Spain related to Research and Universities
  • : Community of Madrid, Spain (regional funding)
  • : Universidad Complutense de Madrid
  • SFERA:Métodos formales escalables para aplicaciones en entornos reales, ref: PID2021-122830OB-C41. Ministerio de Ciencia, Innovación y Universidades. 2022-2025
  • FORTE-CM:FORmal models and Technologies for Emerging applications, ref: S2018/TCS-4314. Comunidad de Madrid y Fondos EIE de la Unión Europea. 2019-2022
  • FREETech:Razonamiento Formal Para Tecnologias Facilitadoras Y Emergente, ref: RTI2018-094403-B-C31. Ministerio De Ciencia, Innovación y Universidades. 2019-2022. 2019-2022
  • LoBaSS:Soluciones Efectivas basadas en la Lógica, ref: TIN2015-69175-C4-2-R. Ministerio de Economía y Competitividad. 2016-2018
  • SOCIAL-REDDATA:¿Nos dirigimos hacia una sociedad desintermediada? Un estudio de la participación social mediante análisis de redes, big data y aprendizaje automático, ref: PR26/16-21B-2. Banco Santander-Universidad Complutense de Madrid. 2016-2018
  • SICOMORo-CM:SIstemas COnfiables mediante Modelos y herRamientas avanzadas, ref: S2013/ICE-3006. Comunidad de Madrid. 2014-2018
  • TELCO:Tecnicas Escalables para la Validacion de Aplicaciones Concurrentes, ref: TIN2012-38137-C02-02. Ministerio de Economía y Competitividad. 2013-2017
  • ENVISAGE:Engineering Virtualized Services, ref: FP7 610582. European Community, FP7. 2013-2016
  • DOVES:Desarrollo de Software Verificable y Eficiente, ref: TIN2008-05624. Ministerio de Economía y Competitividad. 2009-2014
  • PROMETIDOS-CM:Programa de Métodos Rigurosos de Desarrollo de Software de la CM. ref: S2009/TIC-1465. Comunidad de Madrid. 2010-2013
  • SUPRA:Resolucion de Relaciones de Coste Utilizando Tecnicas de Analisis de Programas, ref: PRI-AIBDE-2011-0900. Ministerio de Economía y Competitividad. 2011-2013
  • STAMP:Software Tools and Multiparadigm Programming, ref: TIN2008-06622-C03-01. MINISTERIO DE CIENCIA E INNOVACIÓN. 2009-2012
  • GPD:Grupo de Programación Declarativa, ref: UCM-BSCH-GR35/10-A-910502. Universidad Complutense de Madrid-Banco Santander. 2011.
  • GPD:Grupo de Programación Declarativa, ref: UCM-BSCH-GR58/08-910502. Universidad Complutense de Madrid-Banco Santander. 2009-2010
  • PROMESAS-CM:Programa en métodos para el desarrollo de software fiable, de alta calidad y seguro de la Comunidad de Madrid, ref: S-0505/TIC/0407. Comunidad de Madrid. 2006-2009.
  • FORMS-UCM:Métodos Formales en Sistemas Software Heterogéneos, ref: TIN2005-09207-C03-03. Ministerio de Educación y Ciencia. 2005-2009

Research interests:

  • Static Program Analysis
  • Programming Language Semantics
  • Declarative Debugging
  • Formal Methods

Systems

FORVES (Formally Verified EVM Block-Optimizations)
FORVES is a verification tool to automatically prove the correctness of EVM (Ethereum Virtual Machine) block-optimizations on Ethereum smart contracts using the Coq proof assistant. The EVM equivalence verifier takes two blocks of jump-free EVM instructions, the original block and the optimized one, as well as the initial stack size, and determines if they are equivalent, i.e., if they have the same semantic behavior. Extensions to handle context information from previous blocks is available at FORVES 2.0. Presented at CAV 2023.
LearnSQL
Automatic judge for database learning. LearnSQL provides a simple web interface where students can browse the collections and problems, as well as submit their solutions by writing code in a text area. One of the key design features of LearnSQL is that it is an automatic judge for learning, so it provides detailed feedback when the student submits an incorrect solution. Apart from the evaluation based on execution in an Oracle database, LearnSQL also provides richer feedback through a semantic analysis of the student's code using the Datalog Educational System (DES). Its development and evaluation have been supported by the teaching innovation projects of the Complutense University of Madrid: INNOVA-Docencia 2020-21/18 and INNOVA-Docencia 2021-22/387.
LOBER (LOwer-Bound synthesizER)
Framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. The analysis searches for a metering function that under-approximates the number of loop iterations. The key novelty of our framework is the specialization of loops, which is achieved by restricting their enabled transitions to a subset of the inputs combined with the narrowing of their transition scopes. We also propose a Max-SMT encoding that takes advantage of the use of soft constraints to force the solver look for more accurate solutions. Presented at CAV 2021.
MaxCore (Max-SMT based termination analyzer + COst Recurrence Equation solver)
Cost analyzer that computes upper-bounds for C programs. It combines three components: VeryMax (winner of TermComp'19 for C programs) produces the termination proofs, our implementation generates from them linearly-bounded cost relation systems (LB-CRS) that are fed to CoFloCo or PUBS to produce the upper bounds. Presented at ICLP 2019.
SACO (Static Analyzer for Concurrent Objects)
Static analyzer for Concurrent Objects represented using the ABS modeling language. SACO is able to infer both liveness (namely termination and resource boundedness) and safety properties (namely deadlock freedom) of programs based on concurrent objects. The system integrates auxiliary analyses such as points-to and may-happen-in-parallel, which are essential for increasing the accuracy of the aforementioned more complex properties. It includes the contributions presented in ATVA 2013, ACM Trans. Comput. Log. 17(2), and J. Autom. Reason. 59(1).
Erlang Declarative Debugger (edd)
A declarative (algorithmic) debugger for the sequential part of Erlang. This debugger asks the programmers questions about the expected results of function calls and points out the program fragment that is causing the bug. It includes the contributions presented in TACAS 2014, Sci. Comput. Program. 110, J. Log. Algebraic Methods Program. 101, J. Log. Algebraic Methods Program. 107, and Inf. Softw. Technol. 129.
Toy 2.3.1c << Liberal Types Edition >>
Branch of the Toy system including the type system with liberal type system presented in APLAS 2010 and Math. Struct. Comput. Sci. 25(4). It allows programmers to write type-indexed functions, generic functions, use exitential types, etc. The most remarkable property is the maximal liberality, which states that the type system is the most liberal possible to guarantee type preservation.
Toy 2.3.1b << Safe Opaque Patterns Edition >>
Branch of the Toy system including the type system presented in WFLP 2009 and Inf. Comput. 235, which safely deals with opaque patterns.
Toy: a Constraint Functional Logic System
TOY is a constraint functional logic system, designed to support the main declarative programming styles and their combination. It has been designed and developed mainly by the Declarative Programming Group at the Universidad Complutense de Madrid with collaboration and inputs from colleagues of the Universidad de Málaga.
GPUsart: algebraic reconstruction using CUDA (Spanish)
This is an implementation of a well known algebraic reconstruction algorithm (Simultaneous Algebraic Reconstruction Technique, SART) in CPU and GPU. This kind of algorithms are used for reconstructing the 3D composition of an object from a set of 2D projections of that object. Using the computational resources of the graphics proccessing units (in our case using NVIDIA CUDA technology) we achieve an average increment of speed of about 5000%.