Inicio > Miembros > ELP

ELP

GRUPO DE EXTENSIONES DE LA PROGRAMACIÓN LÓGICA

contacto

María Alpuente

dirección

Departamento de Sistemas Informáticos y Computación
U. Politécnica de Valencia
Camino de Vera S/N
46.020 Valencia

Capacidades en Habilitadores Tecnológicos

Ciber Conectividad

  • Cyber-Physical Systems (Embedded systems, Real-time systems, Safety-critical systems)
  • Cyber-Physical Systems (Embedded systems, Real-time systems, Safety-critical systems)

Ciber Seguridad

  • Security & Privacy By Design tools (automated security verification, automated vulnerability discovery & analysis)
  • Security & Privacy By Design tools (automated security verification, automated vulnerability discovery & analysis)

Inteligencia Artificial y Computación

  • Data generation and handling technologies (Data mining, Modelling&Simulation, Digital Twins)
  • Data generation and handling technologies (Data mining, Modelling&Simulation, Digital Twins)

GRUPO DE EXTENSIONES DE LA PROGRAMACIÓN LÓGICA

El grupo ELP desarrolla tecnología ágil para el análisis, transformación, verificación, depuración, validación, síntesis, certificación y optimización automática de programas, modelos y datos. Algunos de sus logros más recientes están relacionados con el análisis de propiedades de programas y protocolos criptográficos, técnicas y herramientas de análisis y verificación de software, evaluación y calibración de clasificadores de datos, y diagnóstico y reparación automática de sistemas complejos.

Habilitadores Tecnológicos

  • Industrial Formal Methods (program verification, safety analysis, provable security)
    Motivation: Contributing to eradicate software failures that might otherwise lead to security vulnerabilities
    and/or computing errors
    Objective: Formal techniques and automated tools to guarantee software quality and trustworthiness
    Keywords: Symbolic execution, Abstract Interpretation, SAT/SMT, Model checking, Program transformation
  • Protocol crypto-analysis
    Motivation: Analysis of cryptographic communication protocols
    Objective: Extending the state-of-the art protocol analyzer Maude-NPA with further capabilities (SMT
    solving, elliptic curves, etc)
    Keywords: Symbolic model checking, reachability analysis. narrowing
  • Metamodels for Adversarial Machine Learning
    Motivation: Reconciling transparency and privacy in Machine Learning
    Objective: Extracting intrinsic (meta-)characteristics of black-box ML models in order to identify weaknesses,
    vulnerabilities or gaps, and improving system’s security and privacy by providing countermeasures
    Keywords: Data mining automation, Model adaptation, Hierarchical and Multiclass classification, Machine Intelligence Evaluation
  • Applications
    Automated analysis, modeling, verification, learning, debugging and optimization of complex systems
    Confidential and security-sensitive applications (e.g., spam/fraud detection, credit score models, facial
    recognition systems, and network anomaly detection)
    Acrónimo Nombre de la organización

Proyectos / productos / historias de éxito destacados:

  • Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA
    AFOSR (Air Force Office of Scientific Research, US) FA9550-17-1-0286
    NOTICIAS: LEVANTE | 20MINUTOS | UPV | I+D |
  • Who's behind these predictions? Reconciling transparency and privacy in machine learning
    AFOSR (Air Force Office of Scientific Research, US) FA9550-17-1-0287
    NOTICIAS: El Confidencial | Levante
  • Paradigms of Artificial General Intelligence and Their Associated Risks
    US Elon Musk grant though the Future of Life Institute
    NOTICIAS: BBC | Nature | Future of Life

Activos disponibles: Infraestructuras y equipamiento:

  • Laboratorios e infraestructuras tecnológicas para desarrollo, experimentación y validación de nuevos
    productos o servicios basados en tecnologías habilitadoras.
  • Equipamiento para la producción de prototipos.